proposition: Lemma edivp_def p q : edivp p q = (scalp p q, divp p q, modp p q).
proof: Proof. by rewrite /scalp /divp /modp; case: (edivp p q) => [[]] /=. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)