proposition: Lemma is_C_RInt_unique (f : R -> C) (a b : R) (l : C) : is_RInt f a b l -> C_RInt f a b = l.
proof: Proof. intros Hf. apply RInt_fct_extend_pair with (3 := Hf). by apply is_RInt_unique. by apply is_RInt_unique. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)