proposition: Lemma ffact_le_expn m p : p ^_ m <= p ^ m.
proof: Proof. elim: m p => [|m IHm] p //. by rewrite ffactnSr expnSr; apply/leq_mul/leq_subr/IHm. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) mathcomp(bigenough)