proposition: Lemma dvdp_gcd_idl m n : m %| n -> gcdp m n %= m.
proof: Proof. have [-> | mn0] := eqVneq m 0. by rewrite dvd0p => /eqP ->; rewrite gcdp0 eqpxx. rewrite dvdp_eq; move/eqP/(f_equal (gcdp m)) => h. apply: eqp_trans (gcdp_mull (n %/ m) _). by rewrite -h eqp_sym gcdp_scaler // expf_neq0 // lead_coef_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)