Committing all the recent development of Andrea after the merge between his

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

diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index d269e5fe1b83485fc20203ef08c5e3e6d7c988aa..4ec4dfc5b11089876cafc3d2802a80f098c3917a 100644 (file)
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -52,6 +52,15 @@ qed.
 theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
 \def transitive_le.
 
+theorem transitive_lt: transitive nat lt.
+simplify.intros.elim H1.
+apply le_S. assumption.
+apply le_S.assumption.
+qed.
+
+theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p
+\def transitive_lt.
+
 theorem le_S_S: \forall n,m:nat. n \leq m \to S n \leq S m.
 intros.elim H.
 apply le_n.
@@ -95,10 +104,11 @@ apply H.assumption.
 apply le_S_S_to_le.assumption.
 qed.
 
-(* ??? this needs not le *)
-theorem S_pred: \forall n:nat.O<n \to n=S (pred n).
-intro.elim n.apply False_ind.exact not_le_Sn_O O H.
-apply eq_f.apply pred_Sn.
+(* not eq *)
+theorem lt_to_not_eq : \forall n,m:nat. n<m \to \lnot (n=m).
+simplify.intros.cut (le (S n) m) \to False.
+apply Hcut.assumption.rewrite < H1.
+apply not_le_Sn_n.
 qed.
 
 (* le vs. lt *)
@@ -108,6 +118,11 @@ apply le_S. apply le_n.
 apply le_S. assumption.
 qed.
 
+theorem lt_S_to_le : \forall n,m:nat. n < S m \to n \leq m.
+simplify.intros.
+apply le_S_S_to_le.assumption.
+qed.
+
 theorem not_le_to_lt: \forall n,m:nat. \lnot (n \leq m) \to m<n.
 intros 2.
 apply nat_elim2 (\lambda n,m.\lnot (n \leq m) \to m<n).
@@ -123,6 +138,19 @@ apply not_le_Sn_n n H1.
 apply H2.apply lt_to_le. apply H3.
 qed.
 
+theorem not_lt_to_le: \forall n,m:nat. Not (lt n m) \to le m n.
+simplify.intros.
+apply lt_S_to_le.
+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).
+apply lt_to_not_le.simplify.
+apply le_S_S.assumption.
+qed.
+
 (* le elimination *)
 theorem le_n_O_to_eq : \forall n:nat. n \leq O \to O=n.
 intro.elim n.reflexivity.
@@ -146,6 +174,29 @@ apply H2.reflexivity.
 apply H3. apply le_S_S. assumption.
 qed.
 
+(* lt and le trans *)
+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.simplify.apply le_S.assumption.
+qed.
+
+theorem le_to_lt_to_lt: \forall n,m,p:nat. le n m \to lt m p \to lt n p.
+intros 4.elim H.
+assumption.apply H2.simplify.
+apply lt_to_le.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.
+qed.
+
+theorem lt_O_n_elim: \forall n:nat. lt O n \to 
+\forall P:nat\to Prop. (\forall m:nat.P (S m)) \to P n.
+intro.elim n.apply False_ind.exact not_le_Sn_O O H.
+apply H2.
+qed.
+
 (* other abstract properties *)
 theorem antisymmetric_le : antisymmetric nat le.
 simplify.intros 2.
@@ -169,3 +220,7 @@ intros 2.simplify.intro.elim H.
 left.apply le_S_S.assumption.
 right.intro.apply H1.apply le_S_S_to_le.assumption.
 qed.
+
+theorem decidable_lt: \forall n,m:nat. decidable (n < m).
+intros.exact decidable_le (S n) m.
+qed.