proposition: Lemma cvgrnyP {R : realType} {T} {F : set_system T} {FF : Filter F} (f : T -> nat) : (((f n)%:R : R) @[n --> F] --> +oo) <-> (f @ F --> \oo).
proof: Proof. split=> [/cvgryPge|/cvgnyPge] Foo. by apply/cvgnyPge => A; near do rewrite -(@ler_nat R); apply: Foo. apply/cvgryPgey; near=> A; near=> n. rewrite (le_trans (@ceil_ge R A))// (ler_int _ _ (f n)) [ceil _]intEsign. by rewrite le_gtF ?expr0 ?mul1r ?lez_nat ?ceil_ge0//; near: n; apply: Foo. 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