proposition: Lemma reciprocal_size p: p`_0 != 0 -> size (reciprocal_pol p) = size p.
proof: Proof. rewrite /reciprocal_pol => td0. apply: size_poly_eq; rewrite prednK ?subnn // size_poly_gt0. by apply /eqP => pz; case /eqP:td0; rewrite pz coefC. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)