proposition: Lemma integral_plus : forall Hfg, Integral (F{+}G) Hfg [=] Integral F contF[+]Integral G contG.
proof: Proof. intros. unfold integral in |- *. eapply eq_transitive_unfolded. 2: apply Lim_plus. apply Lim_wd'; intro; simpl in |- *. unfold integral_seq, Even_Partition_Sum, Partition_Sum in |- *. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply Sumx_plus_Sumx. apply Sumx_wd; intros; simpl in |- *; rational. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)