proposition: Fact pi_subfx_inj : {mono \pi : x / iotaFz x >-> subfx_inj x}.
proof: Proof. unlock subfx_inj => x; apply/eqP; rewrite -/(equiv_subfext _ x). by rewrite -eqmodE reprK. 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)