proposition: Lemma ex_KHInt_const : forall (a b : R) (c : V), ex_KHInt (fun x : R => c) a b.
proof: Proof. intros a b c ; exists (scal (b-a) c) ; apply is_KHInt_const. Qed.
imports: Coq(Reals ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy SF_seq RInt