proposition: Lemma KHInt_correct : forall (f : R -> V) (a b : R), ex_KHInt f a b -> is_KHInt f a b (KHInt f a b).
proof: Proof. intros f a b [v Hv]. unfold KHInt. apply iota_correct. exists v. split. exact Hv. intros w Hw. apply filterlim_locally_unique with (1 := Hv) (2 := Hw). Qed.
imports: Coq(Reals ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy SF_seq RInt