proposition: Lemma C_RInt_segm_plus (f g : C -> C) (z1 z2 : C) : ex_C_RInt_segm f z1 z2 -> ex_C_RInt_segm g z1 z2 -> C_RInt_segm (fun z => f z + g z) z1 z2 = C_RInt_segm f z1 z2 + C_RInt_segm g z1 z2.
proof: Proof. intros Hf Hg. apply is_C_RInt_segm_unique. apply is_C_RInt_segm_plus ; by apply C_RInt_segm_correct. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)