proposition: Lemma exprn_ilt1 n x : 0 <= x -> x < 1 -> x ^+ n < 1 = (n != 0).
proof: Proof. move=> xge0 xlt1. case: n; [by rewrite eqxx ltxx | elim=> [|n ihn]; first by rewrite expr1]. by rewrite exprS mulr_ilt1 // 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)