X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Flt_arith.ma;h=b8339f374e6019dd054719c9928bf735c63aef4b;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=ce66decaa1fb1f51d1bea31db0c6f908737b1849;hpb=63e834c4fbcb3d015f418989ccd6d2fc8c3dd9ab;p=helm.git

diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index ce66decaa..b8339f374 100644
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -21,7 +21,7 @@ theorem monotonic_lt_plus_r:
 \forall n:nat.monotonic nat lt (\lambda m.n+m).
 simplify.intros.
 elim n.simplify.assumption.
-simplify.
+simplify.unfold lt.
 apply le_S_S.assumption.
 qed.
 
@@ -30,9 +30,9 @@ monotonic_lt_plus_r.
 
 theorem monotonic_lt_plus_l: 
 \forall n:nat.monotonic nat lt (\lambda m.m+n).
-change with \forall n,p,q:nat. p < q \to p + n < q + n.
+change with (\forall n,p,q:nat. p < q \to p + n < q + n).
 intros.
-rewrite < sym_plus. rewrite < sym_plus n.
+rewrite < sym_plus. rewrite < (sym_plus n).
 apply lt_plus_r.assumption.
 qed.
 
@@ -41,7 +41,7 @@ monotonic_lt_plus_l.
 
 theorem lt_plus: \forall n,m,p,q:nat. n < m \to p < q \to n + p < m + q.
 intros.
-apply trans_lt ? (n + q).
+apply (trans_lt ? (n + q)).
 apply lt_plus_r.assumption.
 apply lt_plus_l.assumption.
 qed.
@@ -49,32 +49,32 @@ qed.
 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.
+rewrite > (plus_n_O q).assumption.
 apply H.
-simplify.apply le_S_S_to_le.
+unfold lt.apply le_S_S_to_le.
 rewrite > plus_n_Sm.
-rewrite > plus_n_Sm q.
+rewrite > (plus_n_Sm q).
 exact H1.
 qed.
 
 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. 
+intros.apply (lt_plus_to_lt_l n). 
 rewrite > sym_plus.
-rewrite > sym_plus q.assumption.
+rewrite > (sym_plus q).assumption.
 qed.
 
 (* times and zero *)
 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.
+intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
 (* times *)
 theorem monotonic_lt_times_r: 
 \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.
+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 p + (S n1) * p < q + (S n1) * q.
+change with (p + (S n1) * p < q + (S n1) * q).
 apply lt_plus.assumption.assumption.
 qed.
 
@@ -84,9 +84,9 @@ theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q
 theorem monotonic_lt_times_l: 
 \forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
 change with 
-\forall n,p,q:nat. p < q \to p*(S n) < 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).
+rewrite < sym_times.rewrite < (sym_times (S n)).
 apply lt_times_r.assumption.
 qed.
 
@@ -96,44 +96,44 @@ variant lt_times_l: \forall n,p,q:nat. p<q \to p*(S n) < q*(S n)
 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.
+apply (lt_O_n_elim m H).
 intro.
-cut lt O q.
-apply lt_O_n_elim q Hcut.
-intro.change with O < (S m1)*(S m2).
+cut (lt O q).
+apply (lt_O_n_elim q Hcut).
+intro.change with (O < (S m1)*(S m2)).
 apply lt_O_times_S_S.
-apply ltn_to_ltO p q H1.
-apply trans_lt ? ((S n1)*q).
+apply (ltn_to_ltO p q H1).
+apply (trans_lt ? ((S n1)*q)).
 apply lt_times_r.assumption.
-cut lt O q.
-apply lt_O_n_elim q Hcut.
+cut (lt O q).
+apply (lt_O_n_elim q Hcut).
 intro.
 apply lt_times_l.
 assumption.
-apply ltn_to_ltO p q H2.
+apply (ltn_to_ltO p q H2).
 qed.
 
 theorem lt_times_to_lt_l: 
 \forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
 intros.
-cut p < q \lor p \nlt q.
+cut (p < q \lor p \nlt q).
 elim Hcut.
 assumption.
-absurd p * (S n) < q * (S n).
+absurd (p * (S n) < q * (S n)).
 assumption.
 apply le_to_not_lt.
 apply le_times_l.
 apply not_lt_to_le.
 assumption.
-exact decidable_lt p q.
+exact (decidable_lt p q).
 qed.
 
 theorem lt_times_to_lt_r: 
 \forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
 intros.
-apply lt_times_to_lt_l n.
+apply (lt_times_to_lt_l n).
 rewrite < sym_times.
-rewrite < sym_times (S n).
+rewrite < (sym_times (S n)).
 assumption.
 qed.
 
@@ -142,20 +142,20 @@ 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 p=q.
-apply inj_times_r n.assumption.
+intro.absurd (p=q).
+apply (inj_times_r n).assumption.
 apply lt_to_not_eq. assumption.
-intro.absurd q<p.
-apply lt_times_to_lt_r n.assumption.
+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 p<q.
-apply lt_times_to_lt_r n.assumption.
+absurd (p<q).
+apply (lt_times_to_lt_r n).assumption.
 apply le_to_not_lt.apply lt_to_le.assumption.
-intro.absurd q=p.
+intro.absurd (q=p).
 symmetry.
-apply inj_times_r n.assumption.
+apply (inj_times_r n).assumption.
 apply lt_to_not_eq.assumption.
 intro.reflexivity.
 qed.
@@ -163,28 +163,28 @@ qed.
 (* div *) 
 
 theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to n \mod m = O \to O < n / m. 
-intros 4.apply lt_O_n_elim m H.intros.
-apply lt_times_to_lt_r m1.
+intros 4.apply (lt_O_n_elim m H).intros.
+apply (lt_times_to_lt_r m1).
 rewrite < times_n_O.
-rewrite > plus_n_O ((S m1)*(n / (S m1))).
+rewrite > (plus_n_O ((S m1)*(n / (S m1)))).
 rewrite < H2.
 rewrite < sym_times.
 rewrite < div_mod.
 rewrite > H2.
 assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
 theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
 intros.
-apply nat_case1 (n / m).intro.
+apply (nat_case1 (n / m)).intro.
 assumption.intros.rewrite < H2.
 rewrite > (div_mod n m) in \vdash (? ? %).
-apply lt_to_le_to_lt ? ((n / m)*m).
-apply lt_to_le_to_lt ? ((n / m)*(S (S O))).
+apply (lt_to_le_to_lt ? ((n / m)*m)).
+apply (lt_to_le_to_lt ? ((n / m)*(S (S O)))).
 rewrite < sym_times.
 rewrite > H2.
-simplify.
+simplify.unfold lt.
 rewrite < plus_n_O.
 rewrite < plus_n_Sm.
 apply le_S_S.
@@ -194,19 +194,19 @@ apply le_times_r.
 assumption.
 rewrite < sym_plus.
 apply le_plus_n.
-apply trans_lt ? (S O).
-simplify. apply le_n.assumption.
+apply (trans_lt ? (S O)).
+unfold lt. apply le_n.assumption.
 qed.
 
 (* general properties of functions *)
 theorem monotonic_to_injective: \forall f:nat\to nat.
 monotonic nat lt f \to injective nat nat f.
-simplify.intros.
-apply nat_compare_elim x y.
-intro.apply False_ind.apply not_le_Sn_n (f x).
+unfold injective.intros.
+apply (nat_compare_elim x y).
+intro.apply False_ind.apply (not_le_Sn_n (f x)).
 rewrite > H1 in \vdash (? ? %).apply H.apply H2.
 intros.assumption.
-intro.apply False_ind.apply not_le_Sn_n (f y).
+intro.apply False_ind.apply (not_le_Sn_n (f y)).
 rewrite < H1 in \vdash (? ? %).apply H.apply H2.
 qed.