proposition: Lemma edivp_redivp p q : lead_coef q \in GRing.unit = false -> edivp p q = redivp p q.
proof: Proof. by move=> hu; rewrite unlock hu; case: (redivp p q) => [[? ?] ?]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)