proposition: Lemma modp_mull p q : (p * q) %% q = 0.
proof: Proof. have [-> | nq0] := eqVneq q 0; first by rewrite modp0 mulr0. have rlcq : GRing.rreg (lead_coef q) by apply/rregP; rewrite lead_coef_eq0. have hC : GRing.comm q (lead_coef q)%:P by red; rewrite mulrC. by rewrite modpE; case: ifP => ulcq; rewrite RingComRreg.rmodp_mull // scaler0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)