proposition: Lemma Integral_const : forall c (H : Continuous_I Hab [-C-]c), Integral H [=] c[*] (b[-]a).
proof: Proof. intros. unfold Integral in |- *. rstepr (c[*] (b[-]Min a b) [-]c[*] (a[-]Min a b)). apply cg_minus_wd; apply integral_const. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions