proposition: Lemma C_RInt_Chasles (f : R -> C) (a b c : R) : ex_RInt f a b -> ex_RInt f b c -> C_RInt f a b + C_RInt f b c = C_RInt f a c.
proof: Proof. intros Hf1 Hf2. apply sym_eq, is_C_RInt_unique. apply C_RInt_correct in Hf1. apply C_RInt_correct in Hf2. move: (is_RInt_fct_extend_fst _ _ _ _ Hf1) => /= Hf1_1. move: (is_RInt_fct_extend_snd _ _ _ _ Hf1) => /= Hf1_2. move: (is_RInt_fct_extend_fst _ _ _ _ Hf2) => /= Hf2_1. move: (is_RInt_fct_extend_snd _ _ _ _ Hf2) => /= Hf2_2. now apply @is_RInt_Chasles with b ; apply is_RInt_fct_extend_pair. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)