proposition: Lemma is_C_RInt_segm_triangle (f g : C -> C) (z1 z2 z3 : C) : (forall z, complex_segment z1 z2 z -> is_derive g z (f z)) -> (forall z, complex_segment z2 z3 z -> is_derive g z (f z)) -> (forall z, complex_segment z3 z1 z -> is_derive g z (f z)) -> (forall z, complex_segment z1 z2 z -> continuous f z) -> (forall z, complex_segment z2 z3 z -> continuous f z) -> (forall z, complex_segment z3 z1 z -> continuous f z) -> C_RInt_segm f z1 z2 + C_RInt_segm f z2 z3 + C_RInt_segm f z3 z1 = 0.
proof: Proof. intros. erewrite !is_C_RInt_segm_unique ; last first. apply is_C_RInt_segm_derive ; eassumption. apply is_C_RInt_segm_derive ; eassumption. apply is_C_RInt_segm_derive ; eassumption. ring. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)