proposition: Lemma linear_integral : Integral h contH [=] alpha[*]Integral F contF[+]beta[*]Integral G contG.
proof: Proof. assert (H : Continuous_I Hab (alpha{**}F)). Contin. assert (H0 : Continuous_I Hab (beta{**}G)). Contin. apply eq_transitive_unfolded with (Integral _ H[+]Integral _ H0). unfold h in |- *. apply integral_plus. apply bin_op_wd_unfolded; apply integral_comm_scal. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)