proposition: Lemma Diffble_power : forall (J : interval) pJ F G, positive_fun J F -> Diffble J pJ F -> Diffble J pJ G -> Diffble J pJ (F{!}G).
proof: Proof. intros J pJ F G H H0 H1. set (F1 := Deriv _ _ _ H0) in *. set (G1 := Deriv _ _ _ H1) in *. eapply Derivative_imp_Diffble. apply Derivative_power with (F' := F1) (G' := G1). auto. unfold F1 in |- *; apply Deriv_lemma. unfold G1 in |- *; apply Deriv_lemma. Qed.
imports: CoRN.transc.Exponential