proposition: Lemma is_C_RInt_segm_unique (f : C -> C) (z1 z2 l : C) : is_C_RInt_segm f z1 z2 l -> C_RInt_segm f z1 z2 = l.
proof: Proof. intros. unfold C_RInt_segm. rewrite -C_RInt_scal. by apply is_C_RInt_unique. case: (Ceq_dec z1 z2) => Hz. - rewrite Hz. apply ex_RInt_ext with (fun _ => f z2). move => x _. apply f_equal. rewrite -{1}(scal_one (V := C_R_ModuleSpace) z2). replace (one (K := R_Ring)) with ((1-x)+x)%R. by rewrite scal_distr_r. change one with 1 ; ring. apply ex_RInt_const. - eapply ex_RInt_ext. 2: apply (fun f => ex_C_RInt_scal f (/(z2 - z1))). 2: eexists ; apply H. simpl => x _. fold C. field. contradict Hz. replace z2 with (z1 + (z2 - z1)) by ring. rewrite Hz ; ring. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)