There used to be two minimal joins between an ordered_set and an abelian_group:

[helm.git] / matita / library / nat / orders.ma

diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma
index 6ec0c9992a68b18e15976e96e74ef853c2fc04eb..807906bd21abd4572f75e96fa9bd39977a2309e5 100644 (file)
--- a/matita/library/nat/orders.ma
+++ b/matita/library/nat/orders.ma
@@ -163,8 +163,7 @@ apply not_le_to_lt.exact H.
 qed.
 
 theorem le_to_not_lt: \forall n,m:nat. le n m \to Not (lt m n).
-intros.
-change with (Not (le (S m) n)).
+intros.unfold Not.unfold lt.
 apply lt_to_not_le.unfold lt.
 apply le_S_S.assumption.
 qed.
@@ -192,7 +191,23 @@ apply H2.reflexivity.
 apply H3. apply le_S_S. assumption.
 qed.
 
+(* le to eq *)
+lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
+apply nat_elim2
+  [intros.apply le_n_O_to_eq.assumption
+  |intros.apply sym_eq.apply le_n_O_to_eq.assumption
+  |intros.apply eq_f.apply H
+    [apply le_S_S_to_le.assumption
+    |apply le_S_S_to_le.assumption
+    ]
+  ]
+qed.
+
 (* lt and le trans *)
+theorem lt_O_S : \forall n:nat. O < S n.
+intro. unfold. apply le_S_S. apply le_O_n.
+qed.
+
 theorem lt_to_le_to_lt: \forall n,m,p:nat. lt n m \to le m p \to lt n p.
 intros.elim H1.
 assumption.unfold lt.apply le_S.assumption.
@@ -204,6 +219,12 @@ assumption.apply H2.unfold lt.
 apply lt_to_le.assumption.
 qed.
 
+theorem lt_S_to_lt: \forall n,m. S n < m \to n < m.
+intros.
+apply (trans_lt ? (S n))
+  [apply le_n|assumption]
+qed.
+
 theorem ltn_to_ltO: \forall n,m:nat. lt n m \to lt O m.
 intros.apply (le_to_lt_to_lt O n).
 apply le_O_n.assumption.