proposition: Lemma rmodp_mulmr p q : rmodp (p * (rmodp q d)) d = rmodp (p * q) d.
proof: Proof. by rewrite [q in RHS]rdivp_eq mulrDr rmodpD mulrA rmodp_mull add0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)