proposition: Lemma CL_tr : forall a t0 V0, C 0 a -> {y : R -> R & {pr : (D 1 y) | forall (t : R), (nth_derive y pr) t = (a t) * (y t) /\ y t0 = V0}}.
proof: Proof. intros a t0 V0 H ; assert (Hcont : continuity a) by (inversion H ; assumption). assert (forall t0 t, Riemann_integrable a t0 t). intros ; apply continuity_RiemannInt_1. intros ; inversion H ; auto. assert (pr : C 1 (fun t => V0 * exp (@RiemannInt a t0 t (X t0 t)))). apply C_scal; apply (C_comp 1 exp); [apply C_infty_exp | apply derivable_pt_continuity_Riemann_implies_C1] ; reg. exists (fun t => V0 * exp (@RiemannInt a t0 t (X t0 t))) ; exists (C_implies_D _ _ pr). intro t ; split. rewrite <- (derive_pt_RiemannInt a t0 t X (Hcont t)), <-(derive_pt_exp ), <- derive_pt_scal, Rmult_comm, <- (derive_pt_comp (fun t1 => RiemannInt (X t0 t1)) (mult_real_fct V0 exp)) ; apply pr_nu_var ; reflexivity. rewrite RiemannInt_singleton, exp_0 ; apply Rmult_1_r. Qed.
imports: Reals Rintegral Riemann_integrable Rfunction_classes Nth_derivative_def Lra Ring Ranalysis Rextensionality