From 9be9ca06b0050a29f0d5611c2d3254125557e59d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 26 May 2009 10:47:42 +0000 Subject: [PATCH] removed a call to autobatch. --- helm/software/matita/library/Z/moebius.ma | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/library/Z/moebius.ma b/helm/software/matita/library/Z/moebius.ma index b9d12c223..14f2b65e7 100644 --- 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 -- 2.39.2