proposition: Theorem FTC2 : {c : IR | Feq J (G{-}G0) [-C-]c}.
proof: Proof. apply FConst_prop with pJ. apply Derivative_wdr with (F{-}F). FEQ. apply Derivative_minus; auto. apply FTC1. Qed.
imports: CoRN.ftc.MoreIntegrals CoRN.ftc.CalculusTheorems