X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fgeneric_iter_p.ma;h=6956b7fab7b066b472a42e9fbfed1701f0173d8e;hb=a2b703feae630d0fdd1740bd18e80ee1f6654a88;hp=28ef391eb4e6790124601cba297cf7a7ea16c467;hpb=c02d3479aa43b1ddc03c1af111295151acc30d43;p=helm.git

diff --git a/helm/software/matita/library/nat/generic_iter_p.ma b/helm/software/matita/library/nat/generic_iter_p.ma
index 28ef391eb..6956b7fab 100644
--- a/helm/software/matita/library/nat/generic_iter_p.ma
+++ b/helm/software/matita/library/nat/generic_iter_p.ma
@@ -616,7 +616,7 @@ elim n
                   rewrite > H8
                   [ reflexivity
                   | assumption
-                  | autobatch
+                  | apply andb_true_true; [2: apply H12]
                   ]
                 | apply eqb_false_to_not_eq.
                   generalize in match H14.
@@ -915,8 +915,8 @@ cut (O < p)
            rewrite < exp_plus_times.
            apply eq_f.
            rewrite > sym_plus.
-           apply plus_minus_m_m.
-           autobatch
+           apply plus_minus_m_m. 
+           autobatch; 
           ]
         ]
       |intros.
@@ -941,8 +941,8 @@ cut (O < p)
         [apply le_S_S_to_le.
          change with ((i/S m) < S n).
          apply (lt_times_to_lt_l m).
-         apply (le_to_lt_to_lt ? i)
-          [autobatch|assumption]
+         apply (le_to_lt_to_lt ? i);[2:assumption]
+         apply eq_plus_to_le;[2:autobatch]
         |apply le_exp
           [assumption
           |apply le_S_S_to_le.