proposition: Lemma Derivative_I_unique : Derivative_I Hab' F G -> Derivative_I Hab' F H -> Feq I G H.
proof: Proof. intros H0 H1. elim H0; intros incF H2. elim H2; intros incG H3. elim H1; intros incF' H6. elim H6; intros incH H4. clear H0 H2 H6. apply eq_imp_Feq; auto. intros x H0 Hx Hx'. apply cg_inv_unique_2. apply AbsIR_approach_zero; intros e H2. elim (H3 _ (pos_div_two _ _ H2)). intros dg H6 H7. elim (H4 _ (pos_div_two _ _ H2)). clear H4 H3; intros dh H3 H4. set (d := Min (Min dg dh) [1]) in *. elim (Derivative_I_unique_lemma x H0 d). intros y Hy' Hy''. elim Hy''; clear Hy''; intros Hy'' Hy. apply mult_cancel_leEq with (AbsIR (y[-]x)). apply AbsIR_pos; assumption. eapply leEq_wdl. 2: apply AbsIR_resp_mult. set (Hxx := incF x H0) in *. set (Hyy := incF y Hy'') in *. apply leEq_wdl with (AbsIR (F y Hyy[-]F x Hxx[-]H x Hx'[*] (y[-]x) [-] (F y Hyy[-]F x Hxx[-]G x Hx[*] (y[-]x)))). 2: apply un_op_wd_unfolded; rational. eapply leEq_transitive. apply triangle_IR_minus. rstepr (e [/]TwoNZ[*]AbsIR (y[-]x) [+]e [/]TwoNZ[*]AbsIR (y[-]x)). apply plus_resp_leEq_both; [ apply H4 | apply H7 ]; try assumption; eapply leEq_transitive; try apply Hy'; unfold d in |- *; eapply leEq_transitive. apply Min_leEq_lft. apply Min_leEq_rht. apply Min_leEq_lft. apply Min_leEq_lft. unfold d in |- *; repeat apply less_Min; [ assumption | assumption | apply pos_one ]. Qed.
imports: CoRN.ftc.Continuity