proposition: Lemma Gseqlt1 (r : rat)(eps : rat) : 0 < eps -> 0 < r < 1 -> exists N : nat, forall n : nat, (N <= n)%N -> r ^ n < eps.
proof: Proof. move=> ge0eps /andP [lt0r ltr1]. have hE : 0 <= eps ^-1 by apply/ltW; rewrite invr_gt0. have hr : 1 < r ^-1 by rewrite invf_gt1. have [M hM] := Gseqgt1 hE hr; exists M => n hMn. rewrite -ltf_pV2 //; first by rewrite invr_expz -exprz_inv; exact: hM. exact: exprz_gt0. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) mathcomp(bigenough)