X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fgeneric_iter_p.ma;h=7f51ac700c18e1a391e96c03c7462d1db03c536f;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=5f15bddc93e86a452497614bae6fc236d1ebf9a7;hpb=c445ba5534cccde19016c92660ab52777af221c0;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 5f15bddc9..7f51ac700 100644
--- a/helm/software/matita/library/nat/generic_iter_p.ma
+++ b/helm/software/matita/library/nat/generic_iter_p.ma
@@ -158,8 +158,7 @@ iter_p_gen (k + n) p A g baseA plusA
 intros.
 
 elim k
-[ rewrite < (plus_n_O n).
-  simplify.
+[ simplify.
   rewrite > H in \vdash (? ? ? %).
   rewrite > (H1 ?).
   reflexivity
@@ -283,8 +282,7 @@ elim n
           rewrite > sym_plus.
           rewrite > (div_plus_times ? ? ? H5).
           rewrite > (mod_plus_times ? ? ? H5).
-          rewrite > H4.
-          simplify.reflexivity.   
+          reflexivity.   
         ]
       | reflexivity
       ]
@@ -366,8 +364,7 @@ elim n
           rewrite > sym_plus.
           rewrite > (div_plus_times ? ? ? H5).
           rewrite > (mod_plus_times ? ? ? H5).
-          rewrite > H4.
-          simplify.reflexivity.   
+          reflexivity.   
         ]
       | reflexivity
       ]
@@ -619,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.
@@ -919,7 +916,7 @@ cut (O < p)
            apply eq_f.
            rewrite > sym_plus.
            apply plus_minus_m_m.
-           autobatch
+           autobatch by le_S_S_to_le, lt_mod_m_m, lt_O_S;
           ]
         ]
       |intros.
@@ -944,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]
+         autobatch by eq_plus_to_le, div_mod, lt_O_S.
         |apply le_exp
           [assumption
           |apply le_S_S_to_le.
@@ -1571,7 +1568,10 @@ apply (trans_eq ? ?
                 [ assumption
                 | assumption
                 ]
-              | rewrite > H14.
+              | unfold ha.
+                unfold ha12.
+                unfold ha22.
+                rewrite > H14.
                 rewrite > H13.
                 apply sym_eq.
                 apply div_mod.
@@ -1618,18 +1618,23 @@ apply (trans_eq ? ?
                 rewrite > Hcut.
                 assumption
               ] 
-            | rewrite > Hcut1.
+            | unfold ha.
+              unfold ha12.
+              rewrite > Hcut1.
               rewrite > Hcut.
               assumption
             ]
-          | rewrite > Hcut1.
+          | unfold ha.
+            unfold ha22.
+            rewrite > Hcut1.
             rewrite > Hcut.
             assumption            
           ]
         | cut(O \lt m1)
           [ cut(O \lt n1)      
             [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
-              [ apply (lt_plus_r).
+              [ unfold ha.
+                apply (lt_plus_r).
                 assumption
               | rewrite > sym_plus.
                 rewrite > (sym_times (h11 i j) m1).
@@ -1755,7 +1760,4 @@ apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y
     |assumption
     ]
   ]
-qed.
-
-
-
+qed.
\ No newline at end of file