proposition: Lemma is_C_RInt_segm_opp (f : C -> C) (z1 z2 If : C) : is_C_RInt_segm f z1 z2 If -> is_C_RInt_segm (fun z => - f z) z1 z2 (- If).
proof: Proof. unfold is_C_RInt_segm. intros Hf. move: (is_RInt_opp _ _ _ _ Hf). apply is_RInt_ext. intros x _. change opp with Copp. by simpl ; ring_simplify. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)