From 574931a682c742e47d77d7115b7c80bae5857d23 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 21 May 2009 11:42:28 +0000 Subject: [PATCH] autobatch -> autobatch by --- helm/software/matita/library/nat/generic_iter_p.ma | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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. -- 2.39.2