proposition: Lemma gcdp_exp p k l : gcdp (p ^+ k) (p ^+ l) %= p ^+ minn k l.
proof: Proof. case: leqP => [|/ltnW] /subnK <-; rewrite exprD; first exact: gcdp_mull. exact/(eqp_trans (gcdpC _ _))/gcdp_mull. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)