(* *)
(**************************************************************************)
-include "ordered_set.ma".
-
include "nat/compare.ma".
-include "cprop_connectives.ma".
+include "bishop_set.ma".
definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
cases m;[ apply H1| apply H2; apply H3 ]
qed.
+alias symbol "lt" = "natural 'less than'".
lemma nat_discriminable: ∀x,y:nat.x < y ∨ x = y ∨ y < x.
intros (x y); apply (nat_elim2 ???? x y);
[1: intro;left;cases n; [right;reflexivity] left; apply lt_O_S;
[1: intro x; intro; apply (not_le_Sn_n ? H);
|2: apply nat_excess_cotransitive]
qed.
+
+notation "\naturals" non associative with precedence 90 for @{'nat}.
+interpretation "ordered set N" 'nat = nat_ordered_set.
+
+alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)".
+lemma os_le_to_nat_le:
+ ∀a,b:nat_ordered_set.a ≤ b → le a b.
+intros; normalize in H; apply (not_lt_to_le ?? H);
+qed.
+
+lemma nat_le_to_os_le:
+ ∀a,b:nat_ordered_set.le a b → a ≤ b.
+intros 3; apply (le_to_not_lt a b);assumption;
+qed.
+
+lemma nat_lt_to_os_lt:
+ ∀a,b:nat_ordered_set.a < b → lt nat_ordered_set a b.
+intros 3; split;
+[1: apply nat_le_to_os_le; apply lt_to_le;assumption;
+|2: right; apply H;]
+qed.
+
+lemma os_lt_to_nat_lt:
+ ∀a,b:nat_ordered_set. lt nat_ordered_set a b → a < b.
+intros; cases H; clear H; cases H2;
+[2: apply H;| cases (H1 H)]
+qed.
\ No newline at end of file