proposition: Lemma edivpP m d : edivp_spec m d (edivp m d).
proof: Proof. rewrite edivp_def; constructor; first exact: divp_eq. by apply/implyP=> dn0; rewrite ltn_modp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)