proposition: Lemma ler_eXn2l x : 1 < x -> {mono GRing.exp x : m n / (m <= n)%N >-> m <= n}.
proof: Proof. move=> xgt1; apply: (le_mono (inj_homo_lt _ _)); last first. by apply: ler_weXn2l; rewrite ltW. by apply: ieexprIn; rewrite ?gt_eqF ?gtr_cpable //; apply: lt_trans xgt1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)