proposition: Fact subfx_fieldAxiom : forall x, x != 0 -> subfext_inv x * x = 1.
proof: Proof. elim/quotW=> x; apply: contraNeq; rewrite !piE /equiv_subfext /iotaFz !linear0. apply: contraR => nz_x; rewrite poly_rV_K ?size_poly1 // !poly_rV_modp_K. by rewrite iotaPz_modp rmorph1 rmorphM /= iotaPz_modp subfx_poly_invE mulVf. 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)