X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fminus.ma;h=92324aae7610481c69fdc15a3fef5e5da8db0fb2;hb=5c10d402b5de7233bc83d7f685b274832e383212;hp=20785c9e88e87c49b8aa386dd59d8947ef3fbe4e;hpb=4dc47c9675ffd5fa50296ffaa9b5997501518c98;p=helm.git

diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma
index 20785c9e8..92324aae7 100644
--- a/helm/software/matita/library/nat/minus.ma
+++ b/helm/software/matita/library/nat/minus.ma
@@ -267,10 +267,16 @@ qed.
 lemma lt_to_lt_O_minus : \forall m,n.
   n < m \to O < m - n.
 intros.  
-unfold. apply le_plus_to_minus_r. unfold in H. rewrite > sym_plus. 
+unfold. apply le_plus_to_minus_r. unfold in H.
+cut ((S n ≤ m) = (1 + n ≤ m)) as applyS;
+  [ rewrite < applyS; assumption;
+  | demodulate; reflexivity. ]
+(*
+rewrite > sym_plus. 
 rewrite < plus_n_Sm. 
 rewrite < plus_n_O. 
 assumption.
+*)
 qed.  
 
 theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
@@ -357,10 +363,13 @@ theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
 theorem eq_minus_plus_plus_minus: \forall n,m,p:nat. p \le m \to (n+m)-p = n+(m-p).
 intros.
 apply plus_to_minus.
+lapply (plus_minus_m_m ?? H); demodulate. reflexivity.
+(*
 rewrite > sym_plus in \vdash (? ? ? %).
 rewrite > assoc_plus.
 rewrite < plus_minus_m_m.
 reflexivity.assumption.
+*)
 qed.
 
 theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).