proposition: Lemma rdivp_eq p : p = rdivp p d * d + rmodp p d.
proof: Proof. rewrite -rdivp_eq (eqP mond); last exact: commr1. by rewrite expr1n mulr1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)