proposition: Lemma card_Fp_F2 p n' k : let n := n'.+1 in prime p -> k <= n -> (\sum_(x : 'rV['F_p]_n | [forall j : 'I_n, (k <= j) ==> (x ``_ j == 0%R)] && [forall j : 'I_n, (j < k) ==> (x ``_ j != 0%R)]) 1) = (\sum_(x : 'rV['F_2]_n | [forall j : 'I_n, (k <= j) ==> (x ``_ j == 0%R)] && [forall j : 'I_n, (j < k) ==> (x ``_ j != 0%R)]) 1 * p.-1 ^ k).
proof: Proof. move=> n primep kn. destruct p as [|p'] => //; destruct p' as [|p'] => //. set p := p'.+2. transitivity (\sum_(x : 'rV['F_p]_k | [forall j : 'I_k, x ``_ j != 0%R]) 1). rewrite !sum1dep_card. pose f : 'rV_n -> 'rV_k := fun x => (@ulsubmx 'F_p 1 0 k (n - k) (castmx (erefl, esym (subnKC kn)) x)). set D := [set _ | _]. transitivity (#|f @: D|). apply/esym/card_in_imset => /= x y. rewrite !inE => /andP[/forallP xD1 /forallP xD2] /andP[/forallP yD1 /forallP yD2] Hf. apply/rowP => i. case: (leqP k i) => n0i. move: (xD1 i); rewrite n0i implyTb => /eqP /= ->. move: (yD1 i); by rewrite n0i implyTb => /eqP /= ->. move: Hf => /rowP /(_ (Ordinal n0i)). rewrite !mxE !castmxE /= !cast_ord_id !esymK /= !lshift0. set i' := cast_ord _ _. suff -> : i = i' by []. by apply val_inj. apply eq_card => /= x. rewrite !inE; apply/imsetP/forallP => [[y yD -> {x} i]|]. rewrite !mxE !castmxE /=. move: yD. rewrite inE => /andP[/forallP H1 /forallP /(_ (widen_ord kn i))] /=. rewrite (ltn_ord i) implyTb; apply: contra => /eqP H. by rewrite -[X in _ == X]H; apply/eqP; congr (y _ _); apply val_inj. move=> Hx0. exists (castmx (erefl, subnKC kn) (row_mx x (0%R : 'rV_(n - k)))). - rewrite !inE; apply/andP; split; apply/forallP => /= i; apply/implyP => n0i. rewrite castmxE /= cast_ord_id /=. set i' := cast_ord _ _. have @i'' : 'I_(n - k). exists (i - k); destruct k as [|k]; first by rewrite ltn_sub2r. by rewrite subnS prednK // ?subn_gt0 // subnS -subSKn -2!subn1 leq_sub2r // leq_sub2r. rewrite (_ : i' = rshift k i''); last by apply val_inj => /=; rewrite subnKC. by rewrite row_mxEr // mxE. - have := Hx0 (Ordinal n0i). apply: contra. rewrite castmxE /= cast_ord_id. set i' := cast_ord _ _. rewrite (_ : i' = lshift (n - k) (Ordinal n0i)); last by apply val_inj. by rewrite row_mxEl. apply/rowP => i; rewrite !mxE !castmxE /= !cast_ord_id lshift0. rewrite (_ : cast_ord _ _ = (lshift (n - k) i)) ?row_mxEl //; by apply val_inj. transitivity (p.-1 ^ k); last first. rewrite -big_distrl /= sum1dep_card. set s := [set _ | _]. rewrite (_ : s = set1 (\row_(i < n) if k <= i then 0 else 1)%R) ?cards1 ?mul1n //. apply/setP => /= x; rewrite !inE {s}. apply/idP/idP => [/andP[/forallP H1 /forallP H2]|/eqP H]. apply/eqP/rowP => /= j; rewrite !mxE; case: ifPn => n0j. by move: (H1 j); rewrite n0j implyTb => /eqP. rewrite -ltnNge in n0j; move: (H2 j); rewrite n0j implyTb => /eqP xj0. apply/eqP. rewrite f2.F2_eq1. by apply/eqP. apply/andP; split; apply/forallP => /= j; apply/implyP => n0j; rewrite H mxE; by [rewrite n0j | rewrite leqNgt n0j]. by apply: card_rV_wo_zeros. Qed.
imports: Reals mathcomp(all_ssreflect fingroup zmodp ssralg finalg perm matrix) mathcomp(poly mxalgebra mxpoly) mathcomp(Rstruct) ssr_ext ssralg_ext f2 num_occ natbin ssrR Reals_ext bigop_ext