proposition: Lemma ltn_exp2r m n e : e > 0 -> (m ^ e < n ^ e) = (m < n).
proof: Proof. move=> e_gt0; apply/idP/idP=> [|ltmn]. rewrite !ltnNge; apply: contra => lemn. by elim: e {e_gt0} => // e IHe; rewrite !expnS leq_mul. by elim: e e_gt0 => // [[|e] IHe] _; rewrite ?expn1 // ltn_mul // IHe. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring