proposition: Lemma eqp_modpr d p q : p %= q -> (d %% p) %= (d %% q).
proof: Proof. case/eqpP=> [[c1 c2]] /andP [c1n0 c2n0 e]. have -> : p = (c1^-1 * c2) *: q by rewrite -scalerA -e scalerA mulVf // scale1r. by rewrite modpZr ?eqpxx // mulf_eq0 negb_or invr_eq0 c1n0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)