proposition: Lemma is_C_RInt_segm_const c z1 z2 : is_C_RInt_segm (fun _ => c) z1 z2 ((z2 - z1) * c).
proof: Proof. unfold is_C_RInt_segm. evar_last. apply is_RInt_const. by rewrite Rminus_0_r @scal_one. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)