diff options
Diffstat (limited to 'src/SpecificGen/GFtemplate3mod4')
-rw-r--r-- | src/SpecificGen/GFtemplate3mod4 | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/src/SpecificGen/GFtemplate3mod4 b/src/SpecificGen/GFtemplate3mod4 index 09a0874bd..ccee86d1a 100644 --- a/src/SpecificGen/GFtemplate3mod4 +++ b/src/SpecificGen/GFtemplate3mod4 @@ -372,14 +372,6 @@ Local Transparent Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Definition sqrt_m1 := Eval vm_compute in (pow (encode (F.of_Z _ 2)) (pow2_chain (Z.to_pos ((modulus - 1) / 4)))). -Lemma sqrt_m1_correct : rep (mul sqrt_m1 sqrt_m1) (F.opp 1%F). -Proof. - cbv [rep]. - apply F.eq_to_Z_iff. - vm_compute. - reflexivity. -Qed. - Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb andb. Definition inv_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : |