proposition: Lemma eventually_subseq_loc : forall phi, eventually (fun n => (phi n < phi (S n))%nat) -> filterlim phi eventually eventually.
proof: Proof. intros phi [M Hphi] P [N HP]. exists (N+M)%nat. intros n Hn. apply HP. apply Nat.add_le_mono_l with M. rewrite Nat.add_comm ; apply Nat.le_trans with (1:=Hn). apply Nat.le_trans with (1:=MyNat.le_add_l _ (phi M)). assert (H:(forall x, M+phi M + x <= M+phi (x+M))%nat). induction x as [|x IH]. rewrite Nat.add_0_l Nat.add_0_r. apply Nat.le_refl. rewrite <- plus_n_Sm. apply Nat.le_succ_l. apply Nat.le_lt_trans with (1:=IH). apply Nat.add_lt_mono_l. apply Hphi. apply MyNat.le_add_l. assert (M <= n)%nat. apply Nat.le_trans with (2:=Hn); apply MyNat.le_add_l. specialize (H (n-M)%nat). replace (n-M+M)%nat with n in H. apply Nat.le_trans with (2:=H). rewrite (Nat.add_comm _ (phi M)) -Nat.add_assoc. apply Nat.add_le_mono_l. rewrite Nat.add_comm Nat.sub_add. apply Nat.le_refl. exact H0. now rewrite Nat.sub_add. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy