(**************************************************************************)
-set "baseuri" "cic:/matita/nat/minus".
-
include "nat/le_arith.ma".
include "nat/compare.ma".
[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.
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.