proposition: Lemma KHInt_point : forall (f : R -> V) (a : R), KHInt f a a = zero.
proof: Proof. intros f a. apply is_KHInt_unique. apply: is_KHInt_point. Qed.
imports: Coq(Reals ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy SF_seq RInt