proposition: Lemma rmodp_mulml p q : rmodp (rmodp p d * q) d = rmodp (p * q) d.
proof: Proof. by rewrite [in LHS]mulrC [in RHS]mulrC rmodp_mulmr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)