proposition: Lemma is_KHInt_const : forall (a b : R) (c : V), is_KHInt (fun x : R => c) a b (scal (b-a) c).
proof: Proof. intros a b c. intros P HP. destruct HP as (eps, HPeps). exists (fun x : R => eps). intros ptd Hptd Hptd2. apply HPeps. rewrite Riemann_sum_const. destruct Hptd2 as (Hptd0, Hptd1). destruct Hptd1 as (Hptd1, Hptd2). rewrite Hptd2. rewrite Hptd1. rewrite scal_assoc. replace (mult (sign (b - a)) (Rmax a b - Rmin a b)) with (b-a). apply ball_center. apply sym_eq, sign_min_max. Qed.
imports: Coq(Reals ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy SF_seq RInt