proposition: Lemma schange_odd p : p != 0 -> odd (schange p + (0 < lead_tail_coef p)%R).
proof: Proof. rewrite - lead_coef_eq0 /lead_tail_coef tail_coefE /schange lead_coefE nth_last. by move => h; rewrite schange0_odd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polydiv polyorder path interval polyrcf)