proposition: Lemma ex_KHInt_point : forall (f : R -> V) (a : R), ex_KHInt f a a.
proof: Proof. intros f a ; exists zero ; now apply is_KHInt_point. Qed.
imports: Coq(Reals ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy SF_seq RInt