proposition: Lemma ltr_eXn2l x : 1 < x -> {mono (GRing.exp x) : m n / (m < n)%N >-> m < n}.
proof: Proof. by move=> xgt1; apply: (leW_mono (ler_eXn2l _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)