proposition: Lemma Rseq_cv_even_odd_compat : forall (Un : Rseq) (l : R), Rseq_cv (fun i => Un (2 * i)%nat) l -> Rseq_cv (fun i => Un (S (2 * i))%nat) l -> Rseq_cv Un l.
proof: Proof. intros Un l Heven Hodd eps eps_pos ; destruct (Heven _ eps_pos) as [N1 HN1] ; destruct (Hodd _ eps_pos) as [N2 HN2] ; exists (Nat.max (2 * N1) (S (2 * N2))) ; intros n n_lb ; destruct (n_modulo_2 n) as [[p Hp] | [p Hp]] ; subst. apply HN1 ; assert (H := Nat.max_lub_l _ _ _ n_lb) ; lia. apply HN2 ; assert (H := Nat.max_lub_r _ _ _ n_lb) ; lia. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra