proposition: Lemma rdivp_mull p : rdivp (p * d) d = p.
proof: Proof. by rewrite -[p * d]addr0 rdivp_addl_mul rdiv0p addr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)