proposition: Lemma Derivative_I_plus : Derivative_I Hab' (F{+}G) (F'{+}G').
proof: Proof. elim derF; intros incF H1. elim H1; intros incF' H2. elim derG; intros incG H5. elim H5; intros incG' H6. clear H5 H1. apply Derivative_I_char. Included. Included. intros e He. elim (H2 _ (pos_div_two _ _ He)). intros df H H0. elim (H6 _ (pos_div_two _ _ He)). intros dg H1 H3. clear H2 H6. exists (Min df dg). apply less_Min; assumption. intros. rstepr (e [/]TwoNZ[*]AbsIR (y[-]x)[+]e [/]TwoNZ[*]AbsIR (y[-]x)); simpl in |- *. set (fx := F x (ProjIR1 Hx)) in *. set (fy := F y (ProjIR1 Hy)) in *. set (gx := G x (ProjIR2 Hx)) in *. set (gy := G y (ProjIR2 Hy)) in *. set (f'x := F' x (ProjIR1 Hx')) in *. set (g'x := G' x (ProjIR2 Hx')) in *. apply leEq_wdl with (AbsIR (fy[-]fx[-]f'x[*](y[-]x)[+](gy[-]gx[-]g'x[*](y[-]x)))). eapply leEq_transitive. apply triangle_IR. apply plus_resp_leEq_both; unfold fx, fy, gx, gy, f'x, g'x in |- *; [ apply H0 | apply H3 ]; try assumption; apply leEq_transitive with (Min df dg). assumption. apply Min_leEq_lft. assumption. apply Min_leEq_rht. apply AbsIR_wd; rational. Qed.
imports: CoRN.ftc.Derivative