From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 21 May 2009 11:42:28 +0000 (+0000)
Subject: autobatch -> autobatch by
X-Git-Tag: make_still_working~3953
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=574931a682c742e47d77d7115b7c80bae5857d23;p=helm.git

autobatch -> autobatch by
---

diff --git a/helm/software/matita/library/nat/generic_iter_p.ma b/helm/software/matita/library/nat/generic_iter_p.ma
index 6956b7fab..7f51ac700 100644
--- a/helm/software/matita/library/nat/generic_iter_p.ma
+++ b/helm/software/matita/library/nat/generic_iter_p.ma
@@ -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 by le_S_S_to_le, lt_mod_m_m, lt_O_S;
           ]
         ]
       |intros.
@@ -942,7 +942,7 @@ cut (O < p)
          change with ((i/S m) < S n).
          apply (lt_times_to_lt_l m).
          apply (le_to_lt_to_lt ? i);[2:assumption]
-         apply eq_plus_to_le;[2:autobatch]
+         autobatch by eq_plus_to_le, div_mod, lt_O_S.
         |apply le_exp
           [assumption
           |apply le_S_S_to_le.