proposition: Lemma is_C_RInt_segm_plus (f g : C -> C) (z1 z2 If Ig : C) : is_C_RInt_segm f z1 z2 If -> is_C_RInt_segm g z1 z2 Ig -> is_C_RInt_segm (fun z => f z + g z) z1 z2 (If + Ig).
proof: Proof. unfold is_C_RInt_segm. intros Hf Hg. move: (is_RInt_plus _ _ _ _ _ _ Hf Hg). apply is_RInt_ext. intros x _. change plus with Cplus. by simpl ; ring_simplify. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)