- transcript: bugfix

[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 11585f2065706c33ba70901cd3944c4261ad775c..20785c9e88e87c49b8aa386dd59d8947ef3fbe4e 100644 (file)
--- a/helm/software/matita/library/nat/minus.ma
+++ b/helm/software/matita/library/nat/minus.ma
@@ -13,8 +13,6 @@
 (**************************************************************************)
 
 
-set "baseuri" "cic:/matita/nat/minus".
-
 include "nat/le_arith.ma".
 include "nat/compare.ma".
 
@@ -26,8 +24,7 @@ let rec minus n m \def
        [O \Rightarrow (S p)
         | (S q) \Rightarrow minus p q ]].
 
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural minus" 'minus x y = (cic:/matita/nat/minus/minus.con x y).
+interpretation "natural minus" 'minus x y = (minus x y).
 
 theorem minus_n_O: \forall n:nat.n=n-O.
 intros.elim n.simplify.reflexivity.
@@ -78,13 +75,12 @@ qed.
 
 theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
 intros 2.
-generalize in match n.
-elim m.
+elim m in n ⊢ %.
 rewrite < minus_n_O.apply plus_n_O.
-elim n2.simplify.
+elim n1.simplify.
 apply minus_n_n.
 rewrite < plus_n_Sm.
-change with (S n3 = (S n3 + n1)-n1).
+change with (S n2 = (S n2 + n)-n).
 apply H.
 qed.
 
@@ -296,6 +292,47 @@ apply (lt_minus_to_plus O  a b).
 assumption.
 qed.
 
+theorem lt_minus_to_lt_plus:
+\forall n,m,p. n - m < p \to n < m + p.
+intros 2.
+apply (nat_elim2 ? ? ? ? n m)
+  [simplify.intros.autobatch.
+  |intros 2.rewrite < minus_n_O.
+   intro.assumption
+  |intros.
+   simplify.
+   cut (n1 < m1+p)
+    [autobatch
+    |apply H.
+     apply H1
+    ]
+  ]
+qed.
+
+theorem lt_plus_to_lt_minus:
+\forall n,m,p. m \le n \to n < m + p \to n - m < p.
+intros 2.
+apply (nat_elim2 ? ? ? ? n m)
+  [simplify.intros 3.
+   apply (le_n_O_elim ? H).
+   simplify.intros.assumption
+  |simplify.intros.assumption.
+  |intros.
+   simplify.
+   apply H
+    [apply le_S_S_to_le.assumption
+    |apply le_S_S_to_le.apply H2
+    ]
+  ]
+qed. 
+
+theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n).
+intros.
+apply sym_eq.
+apply plus_to_minus.
+autobatch.
+qed.
+
 theorem distributive_times_minus: distributive nat times minus.
 unfold distributive.
 intros.