X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fminus.ma;h=710418d72644022cb4d799fb95f67354da4af89b;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=1ee70bd39c0a19088ebc2fb1d12dfbdf28add444;hpb=65312e560c25b49336241762107e401e7f9c5c3c;p=helm.git

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 1ee70bd39..710418d72 100644
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -170,7 +170,7 @@ qed.
 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
 intros.apply (lt_O_n_elim n H).intro.
 apply (lt_O_n_elim m H1).intro.
-simplify.apply le_S_S.apply le_minus_m.
+simplify.unfold lt.apply le_S_S.apply le_minus_m.
 qed.
 
 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
@@ -227,17 +227,17 @@ qed.
 
 (* minus and lt - to be completed *)
 theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
-intros 3.apply nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p)).
+intros 3.apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p))).
 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
-simplify.intros.apply False_ind.apply not_le_Sn_O n H.
-simplify.intros.
+simplify.intros.apply False_ind.apply (not_le_Sn_O n H).
+simplify.intros.unfold lt.
 apply le_S_S.
 rewrite < plus_n_Sm.
 apply H.apply H1.
 qed.
 
 theorem distributive_times_minus: distributive nat times minus.
-simplify.
+unfold distributive.
 intros.
 apply ((leb_elim z y)).
   intro.cut (x*(y-z)+x*z = (x*y-x*z)+x*z).