proposition: Lemma redivp_eq q r : size r < size d -> let k := (redivp (q * d + r) d).1.1 in redivp (q * d + r) d = (k, q, r).
proof: Proof. case: (monic_comreg mond)=> Hc Hr /(redivp_eq Hc Hr q). by rewrite (eqP mond) => -> /=; rewrite expr1n !mulr1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)