X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Flt_arith.ma;h=a2e7f6109af689edeb6e87fe5f09345e4ea706f8;hb=24320a56c9cc9e92c0a03475e529b4a54f5d4e14;hp=dd4fdcbf98a1e6e5c0667907c4c080c52b0c5696;hpb=5a702cea95883f7095c16b450e065ccb1714fc5a;p=helm.git

diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index dd4fdcbf9..a2e7f6109 100644
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -18,35 +18,35 @@ include "nat/div_and_mod.ma".
 
 (* plus *)
 theorem monotonic_lt_plus_r: 
-\forall n:nat.monotonic nat lt (\lambda m.plus n m).
+\forall n:nat.monotonic nat lt (\lambda m.n+m).
 simplify.intros.
 elim n.simplify.assumption.
 simplify.
 apply le_S_S.assumption.
 qed.
 
-variant lt_plus_r: \forall n,p,q:nat. lt p q \to lt (plus n p) (plus n q) \def
+variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
 monotonic_lt_plus_r.
 
 theorem monotonic_lt_plus_l: 
-\forall n:nat.monotonic nat lt (\lambda m.plus m n).
-change with \forall n,p,q:nat. lt p q \to lt (plus p n) (plus q n).
+\forall n:nat.monotonic nat lt (\lambda m.m+n).
+change with \forall n,p,q:nat. p < q \to p + n < q + n.
 intros.
 rewrite < sym_plus. rewrite < sym_plus n.
 apply lt_plus_r.assumption.
 qed.
 
-variant lt_plus_l: \forall n,p,q:nat. lt p q \to lt (plus p n) (plus q n) \def
+variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
 monotonic_lt_plus_l.
 
-theorem lt_plus: \forall n,m,p,q:nat. lt n m \to lt p q \to lt (plus n p) (plus m q).
+theorem lt_plus: \forall n,m,p,q:nat. n < m \to p < q \to n + p < m + q.
 intros.
-apply trans_lt ? (plus n q).
+apply trans_lt ? (n + q).
 apply lt_plus_r.assumption.
 apply lt_plus_l.assumption.
 qed.
 
-theorem lt_plus_to_lt_l :\forall n,p,q:nat. lt (plus p n) (plus q n) \to lt p q.
+theorem lt_plus_to_lt_l :\forall n,p,q:nat. p+n < q+n \to p<q.
 intro.elim n.
 rewrite > plus_n_O.
 rewrite > plus_n_O q.assumption.
@@ -57,53 +57,53 @@ rewrite > plus_n_Sm q.
 exact H1.
 qed.
 
-theorem lt_plus_to_lt_r :\forall n,p,q:nat. lt (plus n p) (plus n q) \to lt p q.
+theorem lt_plus_to_lt_r :\forall n,p,q:nat. n+p < n+q \to p<q.
 intros.apply lt_plus_to_lt_l n. 
 rewrite > sym_plus.
 rewrite > sym_plus q.assumption.
 qed.
 
 (* times and zero *)
-theorem lt_O_times_S_S: \forall n,m:nat.lt O (times (S n) (S m)).
+theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m).
 intros.simplify.apply le_S_S.apply le_O_n.
 qed.
 
 (* times *)
 theorem monotonic_lt_times_r: 
-\forall n:nat.monotonic nat lt (\lambda m.times (S n) m).
-change with \forall n,p,q:nat. lt p q \to lt (times (S n) p) (times (S n) q).
+\forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
+change with \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q.
 intros.elim n.
 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
-change with lt (plus p (times (S n1) p)) (plus q (times (S n1) q)).
+change with p + (S n1) * p < q + (S n1) * q.
 apply lt_plus.assumption.assumption.
 qed.
 
-theorem lt_times_r: \forall n,p,q:nat. lt p q \to lt (times (S n) p) (times (S n) q)
+theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q
 \def monotonic_lt_times_r.
 
 theorem monotonic_lt_times_l: 
-\forall m:nat.monotonic nat lt (\lambda n.times n (S m)).
+\forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
 change with 
-\forall n,p,q:nat. lt p q \to lt (times p (S n)) (times q (S n)).
+\forall n,p,q:nat. p < q \to p*(S n) < q*(S n).
 intros.
 rewrite < sym_times.rewrite < sym_times (S n).
 apply lt_times_r.assumption.
 qed.
 
-variant lt_times_l: \forall n,p,q:nat. lt p q \to lt (times p (S n)) (times q (S n))
+variant lt_times_l: \forall n,p,q:nat. p<q \to p*(S n) < q*(S n)
 \def monotonic_lt_times_l.
 
-theorem lt_times:\forall n,m,p,q:nat. lt n m \to lt p q \to lt (times n p) (times m q).
+theorem lt_times:\forall n,m,p,q:nat. n<m \to p<q \to n*p < m*q.
 intro.
 elim n.
 apply lt_O_n_elim m H.
 intro.
 cut lt O q.
 apply lt_O_n_elim q Hcut.
-intro.change with lt O (times (S m1) (S m2)).
+intro.change with O < (S m1)*(S m2).
 apply lt_O_times_S_S.
 apply ltn_to_ltO p q H1.
-apply trans_lt ? (times (S n1) q).
+apply trans_lt ? ((S n1)*q).
 apply lt_times_r.assumption.
 cut lt O q.
 apply lt_O_n_elim q Hcut.
@@ -114,13 +114,12 @@ apply ltn_to_ltO p q H2.
 qed.
 
 theorem lt_times_to_lt_l: 
-\forall n,p,q:nat. lt (times p (S n)) (times q (S n)) \to lt p q.
+\forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
 intros.
-(* convertibility problem here *)
-cut Or (lt p q) (Not (lt p q)).
+cut p < q \lor p \nlt q.
 elim Hcut.
 assumption.
-absurd lt (times p (S n)) (times q (S n)).
+absurd p * (S n) < q * (S n).
 assumption.
 apply le_to_not_lt.
 apply le_times_l.
@@ -130,7 +129,7 @@ exact decidable_lt p q.
 qed.
 
 theorem lt_times_to_lt_r: 
-\forall n,p,q:nat. lt (times (S n) p) (times(S n) q) \to lt p q.
+\forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
 intros.
 apply lt_times_to_lt_l n.
 rewrite < sym_times.
@@ -139,22 +138,22 @@ assumption.
 qed.
 
 theorem nat_compare_times_l : \forall n,p,q:nat. 
-eq compare (nat_compare p q) (nat_compare (times (S n) p) (times (S n) q)).
+nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
 intros.apply nat_compare_elim.intro.
 apply nat_compare_elim.
 intro.reflexivity.
-intro.absurd eq nat p q.
+intro.absurd p=q.
 apply inj_times_r n.assumption.
 apply lt_to_not_eq. assumption.
-intro.absurd lt q p.
+intro.absurd q<p.
 apply lt_times_to_lt_r n.assumption.
 apply le_to_not_lt.apply lt_to_le.assumption.
 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
 intro.apply nat_compare_elim.intro.
-absurd (lt p q).
+absurd p<q.
 apply lt_times_to_lt_r n.assumption.
 apply le_to_not_lt.apply lt_to_le.assumption.
-intro.absurd eq nat q p.
+intro.absurd q=p.
 symmetry.
 apply inj_times_r n.assumption.
 apply lt_to_not_eq.assumption.
@@ -215,4 +214,4 @@ theorem increasing_to_injective: \forall f:nat\to nat.
 increasing f \to injective nat nat f.
 intros.apply monotonic_to_injective.
 apply increasing_to_monotonic.assumption.
-qed.
\ No newline at end of file
+qed.