proposition: Lemma integral_const : forall c H, Integral ( [-C-]c)H [=] c[*] (b[-]a).
proof: Proof. intros. assert (H0 : Continuous_I Hab (c{**}[-C-][1])). Contin. apply eq_transitive_unfolded with (Integral _ H0). apply integral_wd; FEQ. eapply eq_transitive_unfolded. apply integral_comm_scal with (contF := Continuous_I_const a b Hab [1]). apply mult_wdr. apply integral_one. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)