diff options
Diffstat (limited to 'src/Util/NumTheoryUtil.v')
| -rw-r--r-- | src/Util/NumTheoryUtil.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 29fedaa9b..8b8595bb7 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -95,13 +95,13 @@ Proof. apply in_mod_ZPGroup; auto. Qed. -Lemma fermat_inv : forall a, a mod p <> 0 -> (a * (a^(p-2) mod p)) mod p = 1. +Lemma fermat_inv : forall a, a mod p <> 0 -> ((a^(p-2) mod p) * a) mod p = 1. Proof. intros. pose proof (prime_ge_2 _ prime_p). - rewrite Zmult_mod_idemp_r. - replace (a * a ^ (p - 2)) with (a^(p-1)). - 2:replace (a * a ^ (p - 2)) with (a^1 * a ^ (p - 2)) by ring. + rewrite Zmult_mod_idemp_l. + replace (a ^ (p - 2) * a) with (a^(p-1)). + 2:replace (a ^ (p - 2) * a) with (a^1 * a ^ (p - 2)) by ring. 2:rewrite <-Zpower_exp; try f_equal; omega. auto using fermat_little. Qed. |