removed a call to autobatch.

diff --git a/helm/software/matita/library/Z/moebius.ma b/helm/software/matita/library/Z/moebius.ma
index b9d12c2231566ca3a6e45c438264fd9a99f095eb..14f2b65e7a62a6d557a6bdb8a41ecba135891589 100644 (file)
--- a/helm/software/matita/library/Z/moebius.ma
+++ b/helm/software/matita/library/Z/moebius.ma
@@ -348,7 +348,11 @@ lapply (exp_ord (nth_prime (max_prime_factor n)) n)
           (ord_rem n (nth_prime (max_prime_factor n))))
           [apply lt_to_le.assumption
           |apply le_n
-          |autobatch
+          |apply sym_eq.
+           apply p_ord_exp1.apply lt_O_nth_prime_n.
+           apply not_divides_ord_rem.apply lt_S_to_lt. apply H.
+           apply lt_SO_nth_prime_n.rewrite > sym_times.rewrite < Hletin.
+           reflexivity.
           |assumption
           ]
         |left.apply sym_eq.assumption