proposition: Lemma near_infty_natSinv_expn_lt (R : archiFieldType) (e : {posnum R}) : \forall n \near \oo, 1 / 2 ^+ n < e%:num.
proof: Proof. near=> n. rewrite -(@ltr_pM2r _ (2 ^+ n)) // -?natrX ?ltr0n ?expn_gt0//. rewrite mul1r mulVr ?unitfE ?gt_eqF// ?ltr0n ?expn_gt0//. rewrite -(@ltr_pM2l _ e%:num^-1) // mulr1 mulrA mulVr ?unitfE // mul1r. rewrite (lt_trans (archi_boundP _)) // natrX upper_nthrootP //. near: n; eexists; last by move=> m; exact. by []. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule