proposition: Lemma is_RInt_point : forall (f : R -> V) (a : R), is_RInt f a a zero.
proof: Proof. intros f a. apply filterlim_locally. move => eps ; exists (mkposreal _ Rlt_0_1) => ptd _ [Hptd [Hh Hl]]. rewrite Riemann_sum_zero. rewrite scal_zero_r. by apply ball_center. by apply ptd_sort. move: Hl Hh ; rewrite /Rmin /Rmax ; by case: Rle_dec (Rle_refl a) => _ _ ->. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy