proposition: Lemma sum_odd_even_split : forall an n, sum_f_R0 (odds an) n = sum_f_R0 an (S (2 * n)) - sum_f_R0 (evens an) n.
proof: Proof. intros an n. induction n. simpl; unfold odds, evens; simpl; ring. simpl. rewrite IHn. replace (n + S (n + 0))%nat with (S (2 * n)) by ring. unfold odds, evens. simpl. replace (S (S (n + S (n + 0)))) with (S (2 * S n)) by ring. replace (S (S (n + (n + 0)))) with (2 * S n)%nat by ring. replace (S (n + S (n + 0))) with (2 * S n)%nat by ring. ring. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia