Every exception that used to have type string is now a string Lazy.t.

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

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 3b39ed43f1faa363340d95fbfe24ef191c98f15d..0c8780f7e68a50e0b453a5fe2dff09707704c214 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -68,6 +68,18 @@ intros.simplify.reflexivity.
 intros.simplify.apply H.apply le_S_S_to_le.assumption.
 qed.
 
+theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
+intros 2.
+generalize in match n.
+elim m.
+rewrite < minus_n_O.apply plus_n_O.
+elim n2.simplify.
+apply minus_n_n.
+rewrite < plus_n_Sm.
+change with S n3 = (S n3 + n1)-n1.
+apply H.
+qed.
+
 theorem plus_minus_m_m: \forall n,m:nat.
 m \leq n \to n = (n-m)+m.
 intros 2.
@@ -88,14 +100,16 @@ apply H.elim H1.
 apply sym_plus.
 qed.
 
-theorem plus_to_minus :\forall n,m,p:nat.m \leq n \to
+theorem plus_to_minus :\forall n,m,p:nat.
 n = m+p \to n-m = p.
 intros.
 apply inj_plus_r m.
-rewrite < H1.
+rewrite < H.
 rewrite < sym_plus.
 symmetry.
-apply plus_minus_m_m.assumption.
+apply plus_minus_m_m.rewrite > H.
+rewrite > sym_plus.
+apply le_plus_n.
 qed.
 
 theorem minus_S_S : \forall n,m:nat.
@@ -237,7 +251,7 @@ theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
 intros.
 cut m+p \le n \or m+p \nleq n.
   elim Hcut.
-    symmetry.apply plus_to_minus.assumption.
+    symmetry.apply plus_to_minus.
     rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m.
       rewrite > sym_plus.rewrite < plus_minus_m_m.
         reflexivity.
@@ -259,8 +273,6 @@ p+(n-m) = n-(m-p).
 intros.
 apply sym_eq.
 apply plus_to_minus.
-apply le_plus_to_minus.
-apply trans_le ? n.assumption.rewrite < sym_plus.apply le_plus_n.
 rewrite < assoc_plus.
 rewrite < plus_minus_m_m.
 rewrite < sym_plus.