proposition: Lemma KHInt_const : forall (a b : R) (v : V), KHInt (fun _ => v) a b = scal (b - a) v.
proof: Proof. intros a b v. apply is_KHInt_unique. apply: is_KHInt_const. Qed.
imports: Coq(Reals ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy SF_seq RInt