X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fcompare.ma;h=3a8e4a87ca50a7416e2df5f72920ea151977f41c;hb=b9af9f1c0de6a1735b492f5c793a87a8fce218cc;hp=60a9d4194c2dc5b3dbf47936260f9763d4bf577d;hpb=3eff4cc36820df9faddb3cb16390717851db499c;p=helm.git

diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma
index 60a9d4194..3a8e4a87c 100644
--- a/helm/matita/library/nat/compare.ma
+++ b/helm/matita/library/nat/compare.ma
@@ -78,6 +78,21 @@ nat_compare n m = nat_compare (S n) (S m).
 intros.simplify.reflexivity.
 qed.
 
+theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
+intro.elim n.apply False_ind.exact not_le_Sn_O O H.
+apply eq_f.apply pred_Sn.
+qed.
+
+theorem nat_compare_pred_pred: 
+\forall n,m:nat.lt O n \to lt O m \to 
+eq compare (nat_compare n m) (nat_compare (pred n) (pred m)).
+intros.
+apply lt_O_n_elim n H.
+apply lt_O_n_elim m H1.
+intros.
+simplify.reflexivity.
+qed.
+
 theorem nat_compare_to_Prop: \forall n,m:nat. 
 match (nat_compare n m) with
   [ LT \Rightarrow n < m