proposition: Lemma sgp_pinfty_sym p : sgp_pinfty (p \Po -'X) = sgp_minfty p.
proof: Proof. rewrite /sgp_pinfty /sgp_minfty lead_coef_comp ?size_opp ?size_polyX //. by rewrite lead_coefN lead_coefX mulrC. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)