proposition: Lemma eqp_exp p q k : p %= q -> p ^+ k %= q ^+ k.
proof: Proof. move=> pq; elim: k=> [|k ihk]; first by rewrite !expr0 eqpxx. by rewrite !exprS (@eqp_trans (q * p ^+ k)) // (eqp_mulr, eqp_mull). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)