PrimeFieldTheorems fermat inverse lemma: prove admit

1 files changed, 1 insertions, 1 deletions

diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index eb269969d..8835a5d6e 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -184,7 +184,7 @@ Section VariousModPrime.
     intros.
     erewrite (Fq_inv_unique inv_fermat); trivial; split; intros; unfold inv_fermat.
     { replace 2%N with (Z.to_N (Z.of_N 2))%N by auto.
-      rewrite Fq_pow_zero. admit. intro.
+      rewrite Fq_pow_zero. reflexivity. intro.
       assert (Z.of_N (Z.to_N (q-2)) = 0%Z) by (rewrite H0; eauto); rewrite Z2N.id in *; omega. }
     { clear x. rename x0 into x. pose proof (fermat_inv _ _ x) as Hf; forward Hf.
       { pose proof @ZToField_FieldToZ; pose proof @ZToField_mod; congruence. }