proposition: Lemma CL_tr_second_member : forall a b t0 V0, C 0 a -> C 0 b -> {y : R -> R & { pr : (D 1 y) | forall (t : R), (nth_derive y pr) t - (a t) * (y t) = b t /\ y t0 = V0}}.
proof: Proof. intros a b t0 V0 Ha0 Hb0 ; assert (Ha: forall t0 t, Riemann_integrable a t0 t) by (intros ; apply continuity_RiemannInt_1 ; inversion Ha0 ; intuition) ; assert (Hconta : continuity a) by (inversion Ha0 ; assumption) ; assert (Hcontb : continuity b) by (inversion Hb0 ; assumption). assert (Hcontsol : forall t1 t, continuity_pt (b * (comp exp (- (fun t => RiemannInt (Ha t1 t)))))%F t). intros ; reg ; apply (C_continuity _ 1) ; apply derivable_pt_continuity_Riemann_implies_C1 ; assumption. assert (Hsol : forall t1 t0 t, Riemann_integrable (b * (comp exp (- (fun t => RiemannInt (Ha t1 t)))))%F t0 t) by (intros ; apply continuity_RiemannInt_1 ; intuition). assert (pr : C 1 (((fct_cte V0) + (fun t => RiemannInt (Hsol t0 t0 t))) * (comp exp (fun t => RiemannInt (Ha t0 t))))%F). apply C_mult ; [apply C_plus ; [apply C_infty_const |] | apply C_comp ; [apply C_infty_exp |]] ; apply derivable_pt_continuity_Riemann_implies_C1 ; reg ; apply RiemannInt_continuity ; assumption. exists (((fct_cte V0) + (fun t => RiemannInt (Hsol t0 t0 t))) * (comp exp (fun t => RiemannInt (Ha t0 t))))%F ; exists (C_implies_D _ _ pr). intros t ; simpl ; split. assert (Hpr1 : derivable_pt (fun t => RiemannInt (Hsol t0 t0 t)) t) by (apply RiemannInt_derivable_pt ; reg ; apply RiemannInt_continuity ; assumption). assert (Hpr2 : derivable_pt (fun t => RiemannInt (Ha t0 t)) t) by (apply RiemannInt_derivable_pt ; auto). unfold derive ; rewrite (pr_nu_var _ (((fct_cte V0) + (fun t => RiemannInt (Hsol t0 t0 t))) * (comp exp (fun t => RiemannInt (Ha t0 t))))%F _ _ (derivable_pt_mult _ _ _ (derivable_pt_plus _ _ _ (derivable_pt_const V0 t) Hpr1) (derivable_pt_comp _ _ _ Hpr2 (derivable_pt_exp _)))). rewrite derive_pt_mult, derive_pt_comp, derive_pt_exp, derive_pt_RiemannInt_1, derive_pt_plus, derive_pt_const ; unfold plus_fct, comp, fct_cte, mult_fct ; simpl. rewrite derive_pt_RiemannInt_1. ring_simplify ; unfold opp_fct ; rewrite exp_Ropp ; field. apply Rgt_not_eq ; apply exp_pos. apply Hcontsol. apply Hconta. reflexivity. unfold comp, plus_fct, mult_fct, fct_cte ; do 2 rewrite RiemannInt_singleton ; rewrite exp_0 ; ring. Qed.
imports: Reals Rintegral Riemann_integrable Rfunction_classes Nth_derivative_def Lra Ring Ranalysis Rextensionality