proposition: Lemma ltr_iXnr x n : 0 < x -> x < 1 -> (x ^+ n < x) = (1 < n)%N.
proof: Proof. case: n=> [|[|n]] //; first by rewrite expr0 => _ /lt_gtF ->. by move=> x0 x1; rewrite exprS gtr_pMr // ?exprn_ilt1 // ltW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)