proposition: Lemma rdivp_addl_mul_small q r : size r < size d -> rdivp (q * d + r) d = q.
proof: Proof. by move=> Hd; case: (monic_comreg mond)=> Hc Hr; rewrite /rdivp redivp_eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)