proposition: Lemma Gseqgt1 (r : rat)(E : rat) : 0 <= E -> 1 < r -> exists N : nat, forall n : nat, (N <= n)%N -> E < r ^ n.
proof: Proof. move=> ge0E lt1r. pose_big_enough M. exists M => k hMk. have le1r : 1 <= r by rewrite ltW. have {}lt1r : 0 < r - 1 by rewrite subr_gt0. suff aux (n : nat) : n%:Q * (r - 1) - 1 <= r ^ n. apply: lt_le_trans (aux k); rewrite -ltrBDr opprK -ltr_pdivrMr //. have: 0 <= (E + 1) / (r - 1) by apply/divr_ge0/ltW/lt1r/addr_ge0. by move/archi_boundP/lt_trans; apply; rewrite ltr_nat. rewrite -pmulrn /exprz; elim: n => [|n ihn]; first by rewrite mul0r. rewrite mulrSr mulrDl mul1r addrAC -lerBrDr; apply: le_trans ihn _. rewrite exprSr -[r - 1]mul1r -[r in _ * r](subrK 1) mulrDr mulr1 addrAC. by rewrite -mulrBl lerDr pmulr_lge0 // subr_ge0 exprn_ege1. by close. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) mathcomp(bigenough)