proposition: Lemma gcdp_mull m n : gcdp n (m * n) %= n.
proof: Proof. have [-> | nn0] := eqVneq n 0; first by rewrite gcd0p mulr0 eqpxx. have [-> | mn0] := eqVneq m 0; first by rewrite mul0r gcdp0 eqpxx. rewrite gcdpE modp_mull gcd0p size_mul //; case: leqP; last by rewrite eqpxx. rewrite (polySpred mn0) addSn /= -[leqRHS]add0n leq_add2r -ltnS. rewrite -polySpred //= leq_eqVlt ltnS size_poly_leq0 (negPf mn0) orbF. case/size_poly1P=> c cn0 -> {mn0 m}; rewrite mul_polyC. suff -> : n %% (c *: n) = 0 by rewrite gcd0p; apply: eqp_scale. by apply/modp_eq0P; rewrite dvdpZl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)