proposition: Lemma dvdn_Pexp2l p m n : p > 1 -> (p ^ m %| p ^ n) = (m <= n).
proof: Proof. move=> p_gt1; case: leqP => [|gt_n_m]; first exact: dvdn_exp2l. by rewrite gtnNdvd ?ltn_exp2l ?expn_gt0 // ltnW. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)