proposition: Lemma Feq_crit_with_const : forall J pJ F G H, Derivative J pJ F H -> Derivative J pJ G H -> {c : IR | Feq J (F{-}G) [-C-]c}.
proof: Proof. intros. apply FConst_prop with pJ. Derivative_Help; FEQ. Qed.
imports: CoRN.ftc.Rolle CoRN.tactics.DiffTactics3