proposition: Lemma near_infty_natSinv_lt (R : archiFieldType) (e : {posnum R}) : \forall n \near \oo, n.+1%:R^-1 < e%:num.
proof: Proof. near=> n; rewrite -(@ltr_pM2r _ n.+1%:R) // mulVr ?unitfE //. rewrite -(@ltr_pM2l _ e%:num^-1) // mulr1 mulrA mulVr ?unitfE // mul1r. rewrite (lt_trans (archi_boundP _)) // ltr_nat. by near: n; exists (Num.bound e%:num^-1). 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