proposition: Lemma exprn_egt1 n x : 1 < x -> 1 < x ^+ n = (n != 0).
proof: Proof. move=> xgt1; case: n; first by rewrite eqxx ltxx. by elim=> [|n ihn]; rewrite ?expr1// exprS mulr_egt1 // exprn_ge0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)