proposition: Lemma eqp_modpl p q : p %= q -> (p %% d) %= (q %% d).
proof: Proof. case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0 e]. by apply/eqpP; exists (c1, c2); rewrite ?c1n0 //= -!modpZl e. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)