demodulate takes an extra argument 'all', if present it attempts to solve

[helm.git] / helm / software / matita / library / nat / minus.ma

diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma
index 20785c9e88e87c49b8aa386dd59d8947ef3fbe4e..92324aae7610481c69fdc15a3fef5e5da8db0fb2 100644 (file)
--- 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).