* Obsolete debugging comments removed

[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 3acce20afe21277adfab0b15c6d023022afd5da5..7240b7d09ebbc9f18384e68ae1d51f3dffa8021b 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -82,7 +82,7 @@ qed.
 
 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to 
 n = m+p.
-intros.apply trans_eq ? ? ((n-m)+m) ?.
+intros.apply trans_eq ? ? ((n-m)+m).
 apply plus_minus_m_m.
 apply H.elim H1.
 apply sym_plus.
@@ -118,8 +118,8 @@ intros 2.
 apply nat_elim2 (\lambda n,m.n \leq m \to n-m = O).
 intros.simplify.reflexivity.
 intros.apply False_ind.
-(* ancora problemi con il not *)
-apply not_le_Sn_O n1 H.
+apply not_le_Sn_O.
+goal 13.apply H.
 intros.
 simplify.apply H.apply le_S_S_to_le. apply H1.
 qed.
@@ -220,7 +220,7 @@ apply (leb_elim z y).
     apply inj_plus_l (x*z).assumption.
     apply trans_eq nat ? (x*y).
       rewrite < distr_times_plus.rewrite < plus_minus_m_m ? ? H.reflexivity.
-      rewrite < plus_minus_m_m ? ? ?.
+      rewrite < plus_minus_m_m.
         reflexivity.
         apply le_times_r.assumption.
   intro.rewrite > eq_minus_n_m_O.