proposition: Lemma C_RInt_segm_opp (f : C -> C) (z1 z2 : C) : C_RInt_segm (fun z => - f z) z1 z2 = - C_RInt_segm f z1 z2.
proof: Proof. unfold C_RInt_segm. rewrite C_RInt_opp ; ring. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)