proposition: Lemma Integral_plus_Integral : Integral Hab [=] Integral Hac[+]Integral Hcb.
proof: Proof. unfold Integral in |- *. apply eq_transitive_unfolded with (integral _ _ le_abc_b _ Habc_b[-]integral _ _ le_abc_ab _ Habc_ab[-] (integral _ _ le_abc_a _ Habc_a[-]integral _ _ le_abc_ab _ Habc_ab)). apply cg_minus_wd; apply integral_plus_Integral. rstepl (integral _ _ le_abc_b _ Habc_b[-]integral _ _ le_abc_a _ Habc_a). rstepl (integral _ _ le_abc_c _ Habc_c[-]integral _ _ le_abc_ac _ Habc_ac[-] (integral _ _ le_abc_a _ Habc_a[-]integral _ _ le_abc_ac _ Habc_ac) [+] (integral _ _ le_abc_b _ Habc_b[-]integral _ _ le_abc_cb _ Habc_cb[-] (integral _ _ le_abc_c _ Habc_c[-]integral _ _ le_abc_cb _ Habc_cb))). apply eq_symmetric_unfolded; apply bin_op_wd_unfolded; apply cg_minus_wd; apply integral_plus_Integral. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions