Proper_sqrt_3mod4 Proper_sqrt_5mod8

1 files changed, 6 insertions, 0 deletions

diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index bd2000df8..e0dfc8f1a 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -108,6 +108,9 @@ Module F.
 
     Definition sqrt_3mod4 (a : F q) : F q := a ^ Z.to_N (q / 4 + 1).
 
+    Global Instance Proper_sqrt_3mod4 : Proper (eq ==> eq ) sqrt_3mod4.
+    Proof. repeat intro; subst; reflexivity. Qed.
+
     Lemma two_lt_q_3mod4 : 2 < q.
     Proof.
       pose proof (prime_ge_2 q _) as two_le_q.
@@ -174,6 +177,9 @@ Module F.
       then b
       else sqrt_minus1 * b.
 
+    Global Instance Proper_sqrt_5mod8 : Proper (eq ==> eq ) sqrt_5mod8.
+    Proof. repeat intro; subst; reflexivity. Qed.
+
     Lemma eq_b4_a2 (x : F q) (Hex:exists y, y*y = x) :
       ((x ^ Z.to_N (q / 8 + 1)) ^ 2) ^ 2 = x ^ 2.
     Proof.