proposition: Lemma min_subfx_vect : Vector.axiom (size p).-1 subFExtend.
proof: Proof. move/subfx_irreducibleP: irr_p => /=/(_ nz_p) min_p; set d := (size p).-1. have Dd: d.+1 = size p by rewrite polySpred. pose Fz2v x : 'rV_d := poly_rV (sval (sig_eqW (subfxE x)) %% p). pose vFz : 'rV_d -> subFExtend := subfx_eval \o rVpoly. have FLinj: injective subfx_inj by apply: fmorph_inj. have Fz2vK: cancel Fz2v vFz. move=> x; rewrite /vFz /Fz2v; case: (sig_eqW _) => /= q ->. apply: FLinj; rewrite !subfx_inj_eval // {2}(divp_eq q p) rmorphD rmorphM /=. by rewrite !hornerE (eqP pz0) mulr0 add0r poly_rV_K // -ltnS Dd ltn_modpN0. suffices vFzK: cancel vFz Fz2v. by exists Fz2v; [apply: can2_linear Fz2vK | exists vFz]. apply: inj_can_sym Fz2vK _ => v1 v2 /(congr1 subfx_inj)/eqP. rewrite -subr_eq0 -!raddfB /= subfx_inj_eval // => /min_p/implyP. rewrite leqNgt implybNN -Dd ltnS size_poly linearB subr_eq0 /=. by move/eqP/(can_inj rVpolyK). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)