1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "bishop_set.ma".
16 include "nat/compare.ma".
17 include "cprop_connectives.ma".
19 definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
23 (∀ n:nat. R O n) → (∀n:nat. R (S n) O) → (∀n,m:nat. R n m → R (S n) (S m)) →
25 intros 5;elim n; [apply H]
26 cases m;[ apply H1| apply H2; apply H3 ]
29 lemma nat_discriminable: ∀x,y:nat.x < y ∨ x = y ∨ y < x.
30 intros (x y); apply (nat_elim2 ???? x y);
31 [1: intro;left;cases n; [right;reflexivity] left; apply lt_O_S;
32 |2: intro;right;apply lt_O_S;
34 [1: cases H1; [left; left; apply le_S_S; assumption]
35 left;right;rewrite > H2; reflexivity;
36 |2: right;apply le_S_S; assumption]]
39 lemma nat_excess_cotransitive: cotransitive ? nat_excess.
40 intros 3 (x y z); unfold nat_excess; simplify; intros;
41 cases (nat_discriminable x z); [2: left; assumption] cases H1; clear H1;
42 [1: right; apply (trans_lt ??? H H2);
43 |2: right; rewrite < H2; assumption;]
46 lemma nat_ordered_set : ordered_set.
47 apply (mk_ordered_set ? nat_excess);
48 [1: intro x; intro; apply (not_le_Sn_n ? H);
49 |2: apply nat_excess_cotransitive]
52 alias id "le" = "cic:/matita/dama/ordered_set/le.con".
53 lemma os_le_to_nat_le:
54 ∀a,b:nat_ordered_set.le nat_ordered_set a b → a ≤ b.
55 intros; normalize in H; apply (not_lt_to_le ?? H);
58 lemma nat_le_to_os_le:
59 ∀a,b:nat_ordered_set.a ≤ b → le nat_ordered_set a b.
60 intros 3; apply (le_to_not_lt a b);assumption;
63 alias id "lt" = "cic:/matita/dama/bishop_set/lt.con".
64 lemma nat_lt_to_os_lt:
65 ∀a,b:nat_ordered_set.a < b → lt nat_ordered_set a b.
67 [1: apply nat_le_to_os_le; apply lt_to_le;assumption;
71 lemma os_lt_to_nat_lt:
72 ∀a,b:nat_ordered_set. lt nat_ordered_set a b → a < b.
73 intros; cases H; clear H; cases H2;
74 [2: apply H;| cases (H1 H)]