]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/library/Z/dirichlet_product.ma
generic version, specializing generic_sigma_p.ma
[helm.git] / helm / software / matita / library / Z / dirichlet_product.ma
index c4706378c24d82de8fa30ac1c3e44a5612fc880c..a1cc3d18e9fdc81a39070fce6e39782fdc722b67 100644 (file)
@@ -162,7 +162,7 @@ apply (trans_eq ? ?
             [apply sym_eq.
              apply div_plus_times.
              assumption
-            |auto
+            |autobatch
             ]
           |apply lt_mod_m_m.
            assumption