proposition: Fact pi_subfext_add : {morph \pi : x y / x + y >-> subfext_add x y}.
proof: Proof. unlock subfext_add => x y /=; apply/eqmodP/eqP. by rewrite /iotaFz !linearD /= !iotaPz_repr. 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)