proposition: Lemma Feq_criterium : forall J pJ F G H, Derivative J pJ F H -> Derivative J pJ G H -> forall x, J x -> (forall Hx Hx', F x Hx [=] G x Hx') -> Feq J F G.
proof: Proof. do 5 intro. intros H0 H1 x H2 H3. elim (Feq_crit_with_const _ _ _ _ _ H0 H1); intros c Hc. apply Feq_transitive with (F{-}G{+}G). FEQ. apply Feq_transitive with ( [-C-][0]{+}G). 2: FEQ. apply Feq_plus. 2: apply Feq_reflexive; Included. apply Feq_transitive with ( [-C-]c). auto. FEQ. rename X into H4. simpl in |- *. elim Hc; intros H5 H6. elim H6; clear H6; intros H7 H6. clear Hc H5 H7 Hx' Hx. simpl in H6. cut (Conj (Dom F) (Dom G) x). intro H5. apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. 2: apply H6 with (Hx := H5); auto. apply eq_symmetric_unfolded; apply x_minus_x; auto. split. exact (Derivative_imp_inc _ _ _ _ H0 _ H2). exact (Derivative_imp_inc _ _ _ _ H1 _ H2). Qed.
imports: CoRN.ftc.Rolle CoRN.tactics.DiffTactics3