proposition: Lemma rreg_size c p : GRing.rreg c -> size (p * c%:P) = size p.
proof: Proof. move=> reg_c; have [-> | nz_p] := eqVneq p 0; first by rewrite mul0r. rewrite size_proper_mul; first by rewrite size_polyC rreg_neq0 ?addn1. by rewrite lead_coefC mulIr_eq0 ?lead_coef_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)