proposition: Lemma Dcomp : forall (Df Dg:R -> Prop) (df dg f g:R -> R) (x0:R), D_in f df Df x0 -> D_in g dg Dg (f x0) -> D_in (fun x:R => g (f x)) (fun x:R => df x * dg (f x)) (Dgf Df Dg f) x0.
proof: Proof. intros Df Dg df dg f g x0 H H0; generalize H H0; unfold D_in; unfold Rdiv; intros; generalize (limit_comp f (fun x:R => (g x - g (f x0)) * / (x - f x0)) ( D_x Df x0) (D_x Dg (f x0)) (f x0) (dg (f x0)) x0); intro; generalize (cont_deriv f df Df x0 H); intro; unfold continue_in in H4; generalize (H3 H4 H2); clear H3; intro; generalize (limit_mul (fun x:R => (g (f x) - g (f x0)) * / (f x - f x0)) (fun x:R => (f x - f x0) * / (x - x0)) (Dgf (D_x Df x0) (D_x Dg (f x0)) f) (dg (f x0)) ( df x0) x0 H3); intro; cut (limit1_in (fun x:R => (f x - f x0) * / (x - x0)) (Dgf (D_x Df x0) (D_x Dg (f x0)) f) (df x0) x0). - intro; generalize (H5 H6); clear H5; intro; generalize (limit_mul (fun x:R => (f x - f x0) * / (x - x0)) ( fun x:R => dg (f x0)) (D_x Df x0) (df x0) (dg (f x0)) x0 H1 (limit_free (fun x:R => dg (f x0)) (D_x Df x0) x0 x0)); intro; unfold limit1_in; unfold limit_in; simpl; unfold limit1_in in H5, H7; unfold limit_in in H5, H7; simpl in H5, H7; intros; elim (H5 eps H8); elim (H7 eps H8); clear H5 H7; intros; elim H5; elim H7; clear H5 H7; intros; split with (Rmin x x1); split. + elim (Rmin_Rgt x x1 0); intros a b; apply (b (conj H9 H5)); clear a b. + intros; elim H11; clear H11; intros; elim (Rmin_Rgt x x1 (Rdist x2 x0)); intros a b; clear b; unfold Rgt in a; elim (a H12); clear H5 a; intros; unfold D_x, Dgf in H11, H7, H10; clear H12; elim (Req_dec (f x2) (f x0)); intro. * elim H11; clear H11; intros; elim H11; clear H11; intros; generalize (H10 x2 (conj (conj H11 H14) H5)); intro; rewrite (Rminus_diag_eq (f x2) (f x0) H12) in H16; rewrite (Rmult_0_l (/ (x2 - x0))) in H16; rewrite (Rmult_0_l (dg (f x0))) in H16; rewrite H12; rewrite (Rminus_diag_eq (g (f x0)) (g (f x0)) (eq_refl (g (f x0)))); rewrite (Rmult_0_l (/ (x2 - x0))); assumption. * clear H10 H5; elim H11; clear H11; intros; elim H5; clear H5; intros; cut (((Df x2 /\ x0 <> x2) /\ Dg (f x2) /\ f x0 <> f x2) /\ Rdist x2 x0 < x1); auto; intro; generalize (H7 x2 H14); intro; generalize (Rminus_eq_contra (f x2) (f x0) H12); intro; rewrite (Rmult_assoc (g (f x2) - g (f x0)) (/ (f x2 - f x0)) ((f x2 - f x0) * / (x2 - x0))) in H15; rewrite <- (Rmult_assoc (/ (f x2 - f x0)) (f x2 - f x0) (/ (x2 - x0))) in H15; rewrite (Rinv_l (f x2 - f x0) H16) in H15; rewrite (let (H1, H2) := Rmult_ne (/ (x2 - x0)) in H2) in H15; rewrite (Rmult_comm (df x0) (dg (f x0))); assumption. - clear H5 H3 H4 H2; unfold limit1_in; unfold limit_in; simpl; unfold limit1_in in H1; unfold limit_in in H1; simpl in H1; intros; elim (H1 eps H2); clear H1; intros; elim H1; clear H1; intros; split with x; split; auto; intros; unfold D_x, Dgf in H4, H3; elim H4; clear H4; intros; elim H4; clear H4; intros; exact (H3 x1 (conj H4 H5)). Qed.
imports: Rbase Rfunctions Rlimit Lra Lia