proposition: Lemma gcdp_scaler c m n : c != 0 -> gcdp m (c *: n) %= gcdp m n.
proof: Proof. move=> cn0; apply: eqp_trans (gcdpC _ _) _. by apply: eqp_trans (gcdp_scalel _ _ _) _ => //; apply: gcdpC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)