From 2644bafe039063e8943e3bd833998549f0b130a6 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Fri, 2 Aug 2024 10:22:57 +0200 Subject: [PATCH] adapt to MC#1229 --- theories/BGappendixC.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/theories/BGappendixC.v b/theories/BGappendixC.v index e39078b..dd4bf95 100644 --- a/theories/BGappendixC.v +++ b/theories/BGappendixC.v @@ -383,8 +383,9 @@ have [q_gt4 | q_le4] := ltnP 4 q. have q3: q = 3%N by apply/eqP; rewrite eqn_leq qgt2 andbT -ltnS -(odd_ltn 5). rewrite (cardsD1 1) E_1 ltnS card_gt0; apply/set0Pn => /=. pose f (c : 'F_p) : {poly 'F_p} := 'X * ('X - 2%:R%:P) * ('X - c%:P) + ('X - 1). -have fc0 c: (f c).[0] = -1 by rewrite !hornerE /= !hornerE. -have fc2 c: (f c).[2%:R] = 1 by rewrite !(subrr, hornerE) /= addrK. +have fc0 c: (f c).[0] = -1 by rewrite !hornerE /= !hornerE; apply/val_inj. +have fc2 c: (f c).[2%:R] = 1. + by rewrite !(subrr, hornerE) /= addrK; apply/val_inj. have /existsP[c nz_fc]: [exists c, ~~ [exists d, root (f c) d]]. have nz_f_0 c: ~~ root (f c) 0 by rewrite /root fc0 oppr_eq0. rewrite -negb_forall; apply/negP=> /'forall_existsP/fin_all_exists[/= rf rfP].