proposition: Lemma is_KHInt_point : forall (f : R -> V) (a : R), is_KHInt f a a zero.
proof: Proof. intros f a. unfold is_KHInt. apply filterlim_ext with (fun ptd : @SF_seq R => @zero V). intro ptd. rewrite Rminus_eq_0 sign_0. rewrite scal_zero_l ; easy. intros P HP. unfold filtermap. destruct HP as (eps, HPeps). exists (fun x : R => {| pos := 1 ; cond_pos := Rlt_0_1 |}). intros ptd Hptd Hptd2. apply HPeps. apply ball_center. Qed.
imports: Coq(Reals ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy SF_seq RInt