proposition: Lemma leq_exp2l m n1 n2 : 1 < m -> (m ^ n1 <= m ^ n2) = (n1 <= n2).
proof: Proof. move=> m_gt1; elim: n1 n2 => [|n1 IHn] [|n2] //; last 1 first. - by rewrite !expnS leq_pmul2l ?IHn // ltnW. - by rewrite expn_gt0 ltnW. by rewrite leqNgt (leq_trans m_gt1) // expnS leq_pmulr // expn_gt0 ltnW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring