proposition: Lemma rreg_div0 q r d : GRing.rreg (lead_coef d) -> size r < size d -> (q * d + r == 0) = (q == 0) && (r == 0).
proof: Proof. move=> reg_d lt_r_d; rewrite addrC addr_eq0. have [-> | nz_q] := eqVneq q 0; first by rewrite mul0r oppr0. apply: contraTF lt_r_d => /eqP->; rewrite -leqNgt size_opp. rewrite size_proper_mul ?mulIr_eq0 ?lead_coef_eq0 //. by rewrite (polySpred nz_q) leq_addl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)