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