proposition: Lemma Rsum_eq_compat : forall Un Vn, Un == Vn -> sum_f_R0 Un == sum_f_R0 Vn.
proof: Proof. intros Un Vn H n. induction n; simpl; rewrite (H _); [|rewrite IHn]; reflexivity. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts MyNat MyRIneq PeanoNat Lra Rtactic