proposition: Lemma ltn_expl m n : 1 < m -> n < m ^ n.
proof: Proof. move=> m_gt1; elim: n => //= n; rewrite -(leq_pmul2l (ltnW m_gt1)) expnS. by apply: leq_trans; apply: ltn_Pmull. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring