From fcd17b377f948b15eec9e23cc15bb6dffb411118 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Thu, 3 Mar 2016 16:17:42 -0500 Subject: tweak to NumTheoryUtil so it builds on older Coq versions --- src/Util/NumTheoryUtil.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 190fd5274..5acef8b75 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -100,7 +100,7 @@ Proof. pose proof (prime_ge_2 _ prime_p). rewrite Zmult_mod_idemp_r. replace (a * a ^ (p - 2)) with (a^(p-1)). - 2:replace a with (a^1) at 2 by ring. + 2:replace (a * a ^ (p - 2)) with (a^1 * a ^ (p - 2)) by ring. 2:rewrite <-Zpower_exp; try f_equal; omega. auto using fermat_little. Qed. -- cgit v1.2.3