proposition: Lemma size_poly_coef_eq0 : forall p q : {poly R}, (forall i, (p`_i == 0) = (q`_i == 0)) -> size p = size q.
proof: Proof. by move=> p q c; apply/eqP; rewrite eqn_leq;apply/andP; split; apply/leq_sizeP => j cj; apply/eqP; (rewrite c || rewrite -c); apply/eqP; move: j cj; apply/leq_sizeP. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)