proposition: Lemma eventually_subseq : forall phi, (forall n, (phi n < phi (S n))%nat) -> filterlim phi eventually eventually.
proof: Proof. intros phi Hphi. apply eventually_subseq_loc. by apply filter_forall. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy