# Library Cpo_nat

``` Require Export Cpo_streams_type. Set Implicit Arguments. ```

# Cpo_nat.v: Domains of natural numbers

``` ```

## Definition

``` ```
• Natural numbers are a particular case of streams over the trivial type unit
``` Lemma unit_eq : forall x : unit, x = tt. destruct x; trivial. Save. Hint Resolve unit_eq. Definition DN : cpo := DS unit. Definition DNS (n : DN) : DN := cons tt n. ```

## Embedding of usual natural numbers

``` Fixpoint nat2DN (n:nat) : DN := match n with 0 => 0 | S p => DNS (nat2DN p) end. ```

## Infinite element

``` CoFixpoint DNinf : DN := DNS DNinf. Lemma DNinf_inv : DNinf = DNS DNinf. pattern DNinf at 1; rewrite (DS_inv DNinf); simpl; trivial. Save. Lemma DNleinf : forall n:DN, n <= DNinf. cofix; destruct n. repeat red; apply DSleEps; apply (DNleinf n). rewrite DNinf_inv. case u. repeat red; apply DSleCon with DNinf. unfold DNS; auto. repeat red; exists O; auto. apply (DNleinf n). Save. Hint Resolve DNleinf. ```

## Properties of basic operators

``` Lemma DNEps_left : forall x y:DN, x == y -> (Eps x :DN) == y. intros; apply Oeq_trans with x; auto. apply Oeq_sym; exact (eqEps x). Save. Lemma DNEps_right : forall x y:DN, x == y -> x == Eps y. intros; apply Oeq_trans with y; auto. exact (eqEps y). Save. Hint Immediate DNEps_left DNEps_right. Lemma DNS_le_compat : forall (x y:DN) , x<=y -> DNS x <= DNS y. intros x y H; exact (DSleCon0 (D:=unit) tt H). Save. Hint Resolve DNS_le_compat. Lemma DNS_eq_compat : forall (x y:DN) , x==y -> DNS x == DNS y. intros; apply Ole_antisym;auto. Save. Hint Resolve DNS_eq_compat. Add Morphism DNS with signature Oeq ==> Oeq as DNS_eq_compat_morph. exact DNS_eq_compat. Save. Lemma DNS_le_simpl : forall x y :DN, DNS x <= DNS y -> x <= y. intros x y H; exact (DSleCon_tl (D:=unit) H). Save. Hint Immediate DNS_le_simpl. Lemma DNS_eq_simpl : forall x y :DN, DNS x == DNS y -> x == y. intros x y H; exact (Con_tl_simpl (D:=unit) H). Save. Hint Immediate DNS_eq_simpl. ```

## Simulation principles

``` Lemma DNle_rec : forall R : DN -> DN -> Prop,    (forall x1 x2 y1 y2:DN, R x1 y1 -> x1==x2 -> y1==y2 -> R x2 y2) ->    (forall s (y:DN), R (DNS s) y -> exists t, y== DNS t /\ R s t)    -> forall x y : DN , R x y -> x <= y. intros R Req RCons x y Rxy. apply DSle_rec_eq with (D:=unit) (R:=R) (x:=x); auto. intro a; rewrite (unit_eq a); intros s y0 H2. case (RCons s y0 H2); intros t (H3,H4); exists t; auto. Save. Lemma DNeq_rec : forall R : DN -> DN -> Prop,    (forall x1 x2 y1 y2:DN, R x1 y1 -> x1==x2 -> y1==y2 -> R x2 y2) ->    (forall s (y:DN), R (DNS s) y -> exists t, y==DNS t /\ R s t)->    (forall s (x:DN), R x (DNS s) -> exists t, x==DNS t /\ R t s)   -> forall x y : DN , R x y -> x == y. intros R Req RCons1 RCons2 x y Rxy;       apply DSeq_rec with (D:=unit) (R:=R); auto. intro a; rewrite (unit_eq a); intros s y0 H2. case (RCons1 s y0 H2); intros t (H3,H4); exists t; auto. intro a; rewrite (unit_eq a); intros s y0 H2. case (RCons2 s y0 H2); intros t (H3,H4); exists t; auto. Save. ```

## More properties on basic functions

``` Lemma DNle_n_Sn : forall x, x <= DNS x. intros; apply DNle_rec with (R:= fun x y => y == DNS x); intros; auto. apply Oeq_trans with y1; auto. apply Oeq_trans with (DNS x1); auto. exists (DNS s); auto. Save. Hint Resolve DNle_n_Sn. Lemma DNinf_le_intro : forall x, DNS x <= x -> DNinf <= x. intros; apply DNle_rec with (R:= fun x y => DNS y <= y); intros; auto. apply Ole_trans with y1; auto. apply Ole_trans with (DNS y1); auto. exists y; auto. Save. Hint Immediate DNinf_le_intro. Lemma is_cons_S : forall n, is_cons n -> n == DNS (rem n). intros; case (is_cons_elim H); intro a; case a; intros (t,H1); auto. apply Oeq_trans with (DNS (rem (cons tt t))). rewrite rem_cons; auto. apply DNS_eq_compat. rewrite H1; trivial. Save. Lemma infinite_S : forall n : DN, DNS n <= n -> infinite n. cofix; intros. assert (is_cons n). apply is_cons_le_compat with (DNS n); unfold DNS; auto. apply inf_intro; trivial. apply infinite_S. apply Ole_trans with (rem (DNS n)); auto. rewrite <- is_cons_S; auto. unfold DNS; rewrite rem_cons; trivial. apply (rem_le_compat (D:=unit)); auto. Save. ```

``` CoFixpoint add (n m : DN) : DN :=      match n with (Eps n') => Eps (add m n')                        | (Con _ n') => DNS (add m n')      end. Lemma add_inv : forall (n m : DN),    add n m = match n with (Eps n') => Eps (add m n')                                      | (Con _ n') => DNS (add m n')    end. intros; rewrite (DS_inv (add n m)); simpl. destruct n; trivial. Save. Lemma add_decomp_elim : forall a (s x y:DN), decomp a s (add x y) ->             exists t, exists u, s = add t u /\                 (x==DNS u /\ y==t \/ x==t /\ y == DNS u). intros a s x y H; case H; clear H; intro k; generalize x y; clear x y; pattern k; apply Wf_nat.lt_wf_ind; intros. rewrite add_inv in H0; destruct x. destruct n; simpl in H0. discriminate H0. case (H n) with (2:=H0); auto; intros t (u,(H1,H2)). exists t; exists u; intuition. rewrite (unit_eq u); exists y; exists x; intuition. rewrite (pred_nthCon (D:=unit) tt (add y x)) in H0. injection H0; auto. Save. Lemma add_eqCons : forall (s x y:DN), add x y == DNS s ->             exists t, exists u, s == add t u /\                 (x==DNS u /\ y==t \/ x == t /\ y == DNS u). intros s x y H; case (decomp_eq (D:=unit) H); intros v (H1,H2). case (add_decomp_elim x y H1); intros t (u, (Heq, H4)). exists t; exists u; intuition. apply Oeq_trans with v; auto. apply Oeq_trans with v; auto. Save. Lemma addS :      forall x' x, DNS x' <= x    -> forall y, (exists s, add x y == DNS s) /\ (exists s, add y x == DNS s). intros x' x H; inversion_clear H. case H0; clear H0; intro k; generalize x; clear x; pattern k; apply Wf_nat.lt_wf_ind; intros. rewrite (add_inv x y); destruct x. destruct n; simpl in H0. discriminate H0. assert  (forall y : DN,     (exists s : DN, add x y == DNS s) /\     (exists s : DN, add y x == DNS s)). intro; apply (H n) with (2:=H0); auto; intros. split. case (H2 y); intros (s,H4) (s',H5); exists s'; auto. rewrite (add_inv y (Eps x)); destruct y. rewrite (add_inv (Eps x) y). case (H2 y); intros (s,H4) (s',H5); exists s'; auto. apply Oeq_trans with (Eps (add y x)); auto. exists (add (Eps x) y); auto. split. exists (add y x); auto. rewrite (add_inv y (Con u x)); case y; intros. rewrite (add_inv (Con u x) d). exists (add d x); auto. exists (add (Con u x) d); auto. Save. Lemma addS_sym :    forall x y v:DN, add x y == DNS v -> exists t', add y x == DNS t'. intros x y v H; case (add_eqCons x y H); intros t (u,(Heq,[(H1,H2)|(H1,H2)])). case (addS (x':=u) (x:=x)) with (y:=y); auto. case (addS (x':=u) (x:=y)) with (y0:=x); auto. Save. ```
DNSn x n = S^n x
``` Fixpoint DNSn (x:DN) (n:nat) {struct n} :DN :=    match n with 0 => x | S p => DNSn (DNS x) p end. Lemma DNSnS : forall n x, DNSn (DNS x) n = DNS (DNSn x n). induction n; simpl; auto. Save. Hint Resolve DNSnS. Lemma DNSn_mon : forall (n:nat) (x y:DN), x<=y -> DNSn x n <= DNSn y n. induction n; simpl; auto; intros. apply IHn; auto. Save. Hint Resolve DNSn_mon. Lemma DNSn_eq_compat : forall (n:nat) (x y:DN), x==y -> DNSn x n == DNSn y n. intros; apply Ole_antisym;auto. Save. Hint Resolve DNSn_eq_compat. ```
Condition S^l x <= z & y <= S^l t ensuring x+y <= z+t
``` Definition compat (x y z t:DN) := exists l:nat, (DNSn x l <= z /\ y <= DNSn t l). Lemma compatS :    forall x y z t x' y' z' t',    compat x y z t ->       (x==DNS y' /\ y==x' \/ x==x' /\ y==DNS y')   -> (z==DNS t' /\ t==z' \/ z==z' /\ t==DNS t')   -> (compat x' y' z' t' \/ compat x' y' t' z' \/ compat y' x' z' t' \/ compat y' x' t' z'). intros x y z t x' y' z' t' (l,(H1,H2)) [(H3,H4) [(H5,H6)|(H5,H6)] |(H3,H4) [(H5,H6)|(H5,H6)]]. repeat right; exists l; split. apply DNS_le_simpl. apply Ole_trans with z; auto. apply Ole_trans with (DNSn (DNS y') l); auto. apply Ole_trans with (DNSn x l); auto. apply Ole_trans with (DNSn t l); auto. apply Ole_trans with y; auto. right;right;left; exists (S l); simpl DNSn; split. apply Ole_trans with z; auto. apply Ole_trans with (DNSn x l); auto. apply Ole_trans with y; auto. apply Ole_trans with (DNSn t l); auto. destruct l; simpl DNSn in H1; simpl DNSn in H2. right;right;left; exists (S 0); simpl DNSn; split. apply Ole_trans with y; auto. apply Ole_trans with t; auto. apply Ole_trans with x; auto. apply Ole_trans with z; auto. right;left; exists l; split; apply DNS_le_simpl. apply Ole_trans with z; auto. apply Ole_trans with (DNSn (DNS x) l); auto. apply Ole_trans with (DNSn (DNS x') l); auto. apply Ole_trans with y; auto. apply Ole_trans with (DNSn (DNS t) l); auto. apply Ole_trans with (DNSn (DNS z') l); auto. left; exists l; split. apply Ole_trans with z; auto. apply Ole_trans with (DNSn x l); auto. apply DNS_le_simpl; apply Ole_trans with y; auto. apply Ole_trans with (DNSn t l); auto. apply Ole_trans with (DNSn (DNS t') l); auto. Save. Lemma compat_addS : forall n m p q v:DN,     (compat n m p q) -> add n m == DNS v -> exists t, add p q == DNS t. intros n m p q v (l,(H,H0)) H1. case (add_eqCons n m H1); intros n' (m',(H2,[(H3,H4)|(H3,H4)])). assert (H5:DNS (DNSn m' l) <= p). rewrite <- DNSnS. apply Ole_trans with (DNSn n l); auto. case (addS H5) with (y:=q); auto. destruct l; simpl DNSn in H; simpl DNSn in H0. assert (H5:DNS m' <= q). apply Ole_trans with m; auto. case (addS H5) with (y:=p); auto. assert (H5:DNS (DNSn n l) <= p). rewrite <- DNSnS; trivial. case (addS H5) with (y:=q); auto. Save. Lemma add_compat :   forall n m p q,     (compat n m p q \/ compat n m q p \/ compat m n p q \/ compat m n q p)     -> add n m <= add p q. intros; apply DNle_rec with      (R:= fun x y => exists n, exists m, exists p, exists q,              x == add n m /\ y == add p q /\              (compat n m p q \/ compat n m q p \/ compat m n p q \/ compat m n q p)). clear H n m p q; intros x1 x2 y1 y2 (n,(m,(p,(q,(H1,(H2,H3)))))). exists n; exists m; exists p; exists q; split. apply Oeq_trans with x1; auto. split; auto. apply Oeq_trans with y1; auto. clear H n m p q; intros s y (n,(m,(p,(q,(H1,(H2,Hc)))))). assert (H1':add n m == DNS s); auto; clear H1. case (add_eqCons n m H1'); intros n' (m', (H4,H5)). case Hc; clear Hc; intro H3. case (compat_addS H3 H1'); intros w H6. case (add_eqCons p q H6); intros p' (q', (H7,H8)). exists w; split; auto. apply Oeq_trans with (add p q); auto. exists n'; exists m'; exists p'; exists q'; split; auto. split; auto. apply (compatS H3 H5 H8). case H3; clear H3; intro H3. case (compat_addS H3 H1'); intros w H6. case (addS_sym q p H6); clear H6 w; intros w H6. case (add_eqCons p q H6); intros p' (q', (H7,H8)). exists w; split; auto. apply Oeq_trans with (add p q); auto. exists n'; exists m'; exists p'; exists q'; split; auto. split; auto. case (compatS H3 (x':=n') (y':=m') (z':=p') (t':=q')); intuition. case (addS_sym n m H1'); intros s' H1. case H3; clear H3; intro H3. case (compat_addS H3 H1); intros w H6. case (add_eqCons p q H6); intros p' (q', (H7,H8)). exists w; split; auto. apply Oeq_trans with (add p q); auto. exists n'; exists m'; exists p'; exists q'; split; auto. split; auto. case (compatS H3 (x':=n') (y':=m') (z':=p') (t':=q')); intuition. case (compat_addS H3 H1); intros w H6. case (addS_sym q p H6); clear H6 w; intros w H6. case (add_eqCons p q H6); intros p' (q', (H7,H8)). exists w; split; auto. apply Oeq_trans with (add p q); auto. exists n'; exists m'; exists p'; exists q'; split; auto. split; auto. case (compatS H3 (x':=n') (y':=m') (z':=p') (t':=q')); intuition. exists n; exists m; exists p; exists q; auto. Save. Lemma add_mon : forall n p m q, n<=p -> m <= q -> add n m <= add p q. intros; apply add_compat. left; exists O; simpl DNSn; auto. Save. Hint Resolve add_mon. Definition Add : DN -m> DN -m> DN := le_compat2_mon add_mon. Lemma Add_simpl : forall x y, Add x y = add x y. trivial. Save. Add Morphism add with signature Oeq ==> Oeq ==> Oeq as add_eq_compat. intros; apply Ole_antisym; auto. Save. Lemma add_le_sym : forall n m, add n m <= add m n. intros; apply add_compat. right; left; exists O; simpl DNSn; auto. Save. Hint Resolve add_le_sym. Lemma add_sym : forall n m, add n m == add m n. intros; apply Ole_antisym; auto. Save. Lemma addS_shift : forall n m, add (DNS n) m == add n (DNS m). intros; apply Ole_antisym; apply add_compat. repeat right; exists (S 0); simpl DNSn; auto. left; exists (S 0); simpl DNSn; auto. Save. Hint Resolve addS_shift. Lemma addS_simpl : forall n m, add (DNS n) m == DNS (add n m). intros; case (addS (x':=n) (x:=DNS n)) with (y:=m); auto; intros (s,H) _. case (add_eqCons (DNS n) m H); intros t (u,(H1,H2)). apply Oeq_trans with (DNS s); auto. apply DNS_eq_compat. apply Oeq_trans with (add t u); intuition. apply Oeq_trans with (add u t); auto. apply add_eq_compat; auto. apply DNS_eq_simpl; auto. rewrite <- H2; rewrite H3; auto. Save. Hint Resolve addS_simpl. Lemma not_le_S_0 : forall n, ~ (DNS n <= 0). exact (not_le_consBot (D:=unit) (a:=tt)). Save. Hint Resolve not_le_S_0. Lemma add_n_0 : forall n, add 0 n == n. intros; apply DNeq_rec with           (R:= fun x y => exists n, x == add 0 n /\ y == n). intros x1 x2 y1 y2 (n0,(H1,H2)) H3 H4. exists n0; intuition eauto. clear n; intros s y (n0,(H1,H2)). assert (Ha:add 0 n0 == DNS s); auto. case (add_eqCons 0 n0 Ha); intros u (v,(He,[(H3,H4)|(H3,H4)])). absurd (DNS v <= 0); auto. exists v; intuition. apply Oeq_trans with n0; auto. exists v; split; auto. rewrite H3; auto. clear n; intros s x (n0,(H1,H2)). assert (Hle:DNS s <= n0); auto. case (addS Hle 0); intros _ (w,Ha). case (add_eqCons 0 n0 Ha); intros u (v,(He,[(H3,H4)|(H3,H4)])). absurd (DNS v <= 0); auto. exists w; intuition. apply Oeq_trans with (add 0 n0); auto. exists v; split. rewrite H3; auto. apply DNS_eq_simpl. apply Oeq_trans with n0; auto. exists n; auto. Save. Lemma add_continuous_right : forall b, continuous (Add b). red; intros b c. apply DNle_rec with      (R:= fun x y => exists b, exists c, x == add b (lub c) /\ y == lub (Add b @c)). intros x1 x2 y1 y2 (b0,(c0,(H1,H2))) H3 H4. exists b0; exists c0; intuition eauto. clear b c; intros s y (b,(c,(H1,H2))). assert (H1':add b (lub c)==DNS s); auto. case (add_eqCons b (lub c) H1'); intros u (v,(He,[(H3,H4)|(H3,H4)])). exists (lub (Add v @ c)); split; auto. apply Oeq_trans with (lub (Add b @ c)); auto. apply Oeq_trans with (lub (c:=DN) (Cons tt @ (Add v @ c))). apply lub_eq_compat; apply fmon_eq_intro; simpl; intros. apply Oeq_trans with (add (DNS v) (c n)). apply add_eq_compat; auto. apply (addS_simpl v (c n)). apply Oeq_sym; apply (lub_comp_eq (D1:=DN) (D2:=DN) (f:=Cons tt)) with         (h:=Add v @ c). exact (Cons_cont tt). exists v; exists c; split; auto. apply Oeq_trans with (add v u); auto. apply Oeq_trans with (add u v); auto. apply add_eq_compat; auto. case (DS_lubCon_inv c H4); intros tlc (Hl1,(m,Hl3)). exists (lub (Add b @ tlc)); split. apply Oeq_trans with (lub (Add b @ c)); auto. apply Oeq_trans with (lub (c:=DN) (Cons tt @ (Add b @ tlc))). apply Oeq_trans with (lub (mseq_lift_right (O:=DN) (Add b @ c) m)); auto. apply lub_eq_compat; apply fmon_eq_intro; unfold mseq_lift_right; simpl; intro. apply Oeq_trans with (add b (Cons tt (tlc n))). apply add_eq_compat; auto. exact (Hl3 n). apply Oeq_trans with (add (DNS b) (tlc n)). apply Oeq_sym; exact (addS_shift b (tlc n)). exact (addS_simpl b (tlc n)). apply Oeq_sym; apply (lub_comp_eq (D1:=DN) (D2:=DN) (f:=Cons tt)) with (h:=(Add b @ tlc)). exact (Cons_cont tt). exists b; exists tlc; split; auto. apply Oeq_trans with (add u v); auto. apply add_eq_compat; auto. exists b; exists c; auto. Save. Lemma add_continuous2 : continuous2 Add. apply continuous2_sym. intros; repeat (rewrite Add_simpl); auto. intros; apply add_continuous_right. Save. Lemma add_continuous : continuous (D2:=DN-M->DN) Add. apply continuous2_continuous. apply add_continuous2. Save. ```

## Length of a stream

``` Definition LENGTH (D:Type) : DS D -c> DN := MAP (fun x:D=>tt). Definition length (D:Type) (s:DS D) : DN := LENGTH D s. Lemma length_simpl : forall (D:Type) (s:DS D), length s = map (fun x:D=>tt) s. trivial. Save. Lemma length_eq_cons : forall D a (s:DS D), length (cons a s) == DNS (length s). intros; repeat rewrite length_simpl. exact (map_eq_cons (fun _ : D => tt) a s). Save. Lemma length_nil : forall D, length (0:DS D) == 0. intro D; exact (map_bot (fun _ : D => tt)). Save. Hint Resolve length_eq_cons length_nil. Lemma length_le_compat : forall D (s t : DS D), s <= t -> length s <= length t. intro D; exact (fcont_monotonic (LENGTH D)). Save. Hint Resolve length_le_compat. Lemma length_eq_compat : forall D (s t : DS D), s == t -> length s == length t. intros; apply Ole_antisym; auto. Save. Hint Resolve length_eq_compat. Add Morphism length with signature Oeq ==> Oeq as length_morph. intros; apply length_eq_compat; trivial. Save. Lemma is_cons_length : forall D (s:DS D), is_cons s -> is_cons (length s). intros; rewrite length_simpl; auto. Save. Hint Resolve is_cons_length. Lemma length_is_cons : forall D (s:DS D), is_cons (length s) -> is_cons s. intros D s; rewrite length_simpl; apply map_is_cons with (F:=fun _:D => tt); auto. Save. Hint Immediate length_is_cons. Lemma length_rem : forall D (s:DS D), length (rem s) == rem (length s). intros; apply (DSeq_intro_is_cons (D:=unit)); intros. assert (is_cons (rem s)); auto. assert (is_cons s); auto. case (is_cons_elim H1); intros a (t,H2). rewrite H2; rewrite length_eq_cons; unfold DNS; repeat rewrite rem_cons; auto. assert (is_cons (length s)); auto. assert (is_cons s); auto. case (is_cons_elim H1); intros a (t,H2). rewrite H2; rewrite length_eq_cons; unfold DNS; repeat rewrite rem_cons; auto. Save. Hint Resolve length_rem. Lemma infinite_length : forall D (s:DS D), infinite s -> infinite (length s). intro D; assert (forall (s:DS D), infinite s -> forall n, n == length s -> infinite n). cofix; intros. case H; intros; apply inf_intro. rewrite H0; auto. apply infinite_length with (rem s); auto. rewrite H0; auto. intros; apply H with s; auto. Save. Hint Resolve infinite_length. Lemma length_infinite : forall D (s:DS D), infinite (length s) -> infinite s. intro D; assert (forall (n:DN), infinite n -> forall (s:DS D), n == length s -> infinite s). cofix; intros. case H; intros; apply inf_intro. assert (is_cons (length s)); auto. rewrite <- H0; auto. apply length_infinite with (rem n); auto. rewrite H0; auto. intros; apply H with (length s); auto. Save. Hint Immediate length_infinite. ```
 Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (58 entries) Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (47 entries) Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (10 entries) Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)

# Global Index

## C

compat [definition, in Cpo_nat]
compatS [lemma, in Cpo_nat]
Cpo_nat [library]

## D

DN [definition, in Cpo_nat]
DNEps_left [lemma, in Cpo_nat]
DNEps_right [lemma, in Cpo_nat]
DNeq_rec [lemma, in Cpo_nat]
DNinf [definition, in Cpo_nat]
DNinf_inv [lemma, in Cpo_nat]
DNinf_le_intro [lemma, in Cpo_nat]
DNleinf [lemma, in Cpo_nat]
DNle_n_Sn [lemma, in Cpo_nat]
DNle_rec [lemma, in Cpo_nat]
DNS [definition, in Cpo_nat]
DNSn [definition, in Cpo_nat]
DNSnS [lemma, in Cpo_nat]
DNSn_eq_compat [lemma, in Cpo_nat]
DNSn_mon [lemma, in Cpo_nat]
DNS_eq_compat [lemma, in Cpo_nat]
DNS_eq_simpl [lemma, in Cpo_nat]
DNS_le_compat [lemma, in Cpo_nat]
DNS_le_simpl [lemma, in Cpo_nat]

## I

infinite_length [lemma, in Cpo_nat]
infinite_S [lemma, in Cpo_nat]
is_cons_length [lemma, in Cpo_nat]
is_cons_S [lemma, in Cpo_nat]

## L

length [definition, in Cpo_nat]
LENGTH [definition, in Cpo_nat]
length_eq_compat [lemma, in Cpo_nat]
length_eq_cons [lemma, in Cpo_nat]
length_infinite [lemma, in Cpo_nat]
length_is_cons [lemma, in Cpo_nat]
length_le_compat [lemma, in Cpo_nat]
length_nil [lemma, in Cpo_nat]
length_rem [lemma, in Cpo_nat]
length_simpl [lemma, in Cpo_nat]

## N

nat2DN [definition, in Cpo_nat]
not_le_S_0 [lemma, in Cpo_nat]

## U

unit_eq [lemma, in Cpo_nat]

# Lemma Index

## C

compatS [in Cpo_nat]

## D

DNEps_left [in Cpo_nat]
DNEps_right [in Cpo_nat]
DNeq_rec [in Cpo_nat]
DNinf_inv [in Cpo_nat]
DNinf_le_intro [in Cpo_nat]
DNleinf [in Cpo_nat]
DNle_n_Sn [in Cpo_nat]
DNle_rec [in Cpo_nat]
DNSnS [in Cpo_nat]
DNSn_eq_compat [in Cpo_nat]
DNSn_mon [in Cpo_nat]
DNS_eq_compat [in Cpo_nat]
DNS_eq_simpl [in Cpo_nat]
DNS_le_compat [in Cpo_nat]
DNS_le_simpl [in Cpo_nat]

## I

infinite_length [in Cpo_nat]
infinite_S [in Cpo_nat]
is_cons_length [in Cpo_nat]
is_cons_S [in Cpo_nat]

## L

length_eq_compat [in Cpo_nat]
length_eq_cons [in Cpo_nat]
length_infinite [in Cpo_nat]
length_is_cons [in Cpo_nat]
length_le_compat [in Cpo_nat]
length_nil [in Cpo_nat]
length_rem [in Cpo_nat]
length_simpl [in Cpo_nat]

## N

not_le_S_0 [in Cpo_nat]

## U

unit_eq [in Cpo_nat]

# Definition Index

## C

compat [in Cpo_nat]

## D

DN [in Cpo_nat]
DNinf [in Cpo_nat]
DNS [in Cpo_nat]
DNSn [in Cpo_nat]

## L

length [in Cpo_nat]
LENGTH [in Cpo_nat]

## N

nat2DN [in Cpo_nat]

# Library Index

## C

Cpo_nat

 Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (58 entries) Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (47 entries) Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (10 entries) Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)