proposition: Lemma is_KHInt_unique : forall (f : R -> V) (a b : R) (l : V), is_KHInt f a b l -> KHInt f a b = l.
proof: Proof. intros f a b l H. apply filterlim_locally_unique with (2 := H). apply KHInt_correct. now exists l. Qed.
imports: Coq(Reals ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy SF_seq RInt