proposition: Lemma Integral_wd' : forall a' b' Ha'b' contF', a [=] a' -> b [=] b' -> Integral contF [=] Integral (a:=a') (b:=b') (Hab:=Ha'b') (F:=F) contF'.
proof: Proof. intros. unfold Integral in |- *. apply cg_minus_wd; apply integral_wd'; try apply bin_op_wd_unfolded; algebra. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions