proposition: Lemma IntegrationBySubstition : forall a b (Hab: Min a b[<=]Max a b) c d (Hcd: c[<]d) (Habcd: included (Compact Hab) (Compact (less_leEq _ _ _ Hcd))) G (HGa: Dom G a) (HGb: Dom G b) G' (HGG': Derivative_I Hcd G G') (HGaGb: Min (G a HGa) (G b HGb)[<=]Max (G a HGa) (G b HGb)) F c0 d0 (Hc0d0: c0[<=]d0) (HGF: maps_into_compacts G F _ _ Hab _ _ Hc0d0) (HFG: Continuous_I Hab ((F[o]G){*}G')) (HF: Continuous_I HGaGb F) (HFc0d0: Continuous_I Hc0d0 F), Integral HFG[=]Integral HF.
proof: Proof. intros. assert(X1:=leEq_less_or_equal _ _ _ Hab). apply not_ap_imp_eq. intros X0. apply X1. clear X1. intros X1. revert X0. apply (eq_imp_not_ap). destruct X1 as [X1|X1]. assert(X:=leEq_less_or_equal _ _ _ Hc0d0). apply not_ap_imp_eq. intros X0. apply X. clear X. intros X. revert X0. apply (eq_imp_not_ap). destruct X as [X|X]. set (J:=clcr c0 d0). assert (HFJ:Continuous J F). eapply (Continuous_Int J Hc0d0 Hc0d0); apply HFc0d0. assert (Jc0:J c0). split. apply leEq_reflexive. assumption. set (F0:=([-S-]HFJ) _ Jc0). assert (dF : Derivative J X F0 F). unfold F0; apply FTC1. apply eq_symmetric. assert (HF':Continuous_I (Min_leEq_Max (G a HGa) (G b HGb)) F). Contin. apply eq_transitive with (Integral HF'). apply Integral_wd'; apply eq_reflexive. set (FGx:=Derivative_imp_inc J X F0 F dF). assert (JGa:J (G a HGa)). destruct HGF as [HGF0 HGF1]. change (Compact Hc0d0 (G a HGa)). apply HGF1. apply compact_Min_lft. assert (JGb:J (G b HGb)). destruct HGF as [HGF0 HGF1]. change (Compact Hc0d0 (G b HGb)). apply HGF1. apply compact_Min_rht. apply eq_transitive with ((F0 (G b HGb) (FGx _ JGb))[-](F0 (G a HGa) (FGx _ JGa))). unfold FGx. apply Barrow. apply HFJ. apply eq_symmetric. assert (HFG':Continuous_I (Min_leEq_Max a b) ((F[o]G){*}G')). Contin. apply eq_transitive with (Integral HFG'). apply Integral_wd'; apply eq_reflexive. set (I:=clcr (Min a b) (Max a b)). assert (dFG:Derivative I X1 (F0[o]G) ((F[o]G){*}G')). apply (Derivative_Int I Hab X1 X1). assert (dF0 : Derivative_I X F0 F). apply (Int_Derivative J Hc0d0 X). assumption. eapply Derivative_I_comp. eapply (included_imp_deriv _ _ Hcd). apply Habcd. apply HGG'. apply dF0. destruct HGF as [HGF0 HGF1]. split. Included. exact HGF1. set (HFGx := Derivative_imp_inc I X1 _ _ dFG). stepr (((F0[o]G) b (HFGx b (compact_Min_rht _ _ Hab)))[-] ((F0[o]G) a (HFGx a (compact_Min_lft _ _ Hab)))). unfold HFGx. apply Barrow. eapply (Continuous_Int I Hab Hab). apply HFG. generalize (HFGx a (compact_Min_lft a b Hab)) (HFGx b (compact_Min_rht a b Hab)). generalize (FGx (G b HGb) JGb) (FGx (G a HGa) JGa). generalize F0 G HGb HGa. clear -a b. intros F G p1 p2 p3 p4 p5 p6. simpl. algebra. assert (Y:G a HGa[=]G b HGb). destruct HGF as [HGF0 HGF1]. apply leEq_imp_eq. apply leEq_transitive with d0. destruct (HGF1 _ HGa (compact_Min_lft _ _ Hab)); assumption. stepl c0; [| assumption]. destruct (HGF1 _ HGb (compact_Min_rht _ _ Hab)); assumption. apply leEq_transitive with d0. destruct (HGF1 _ HGb (compact_Min_rht _ _ Hab)); assumption. stepl c0; [| assumption]. destruct (HGF1 _ HGa (compact_Min_lft _ _ Hab)); assumption. stepl ([0]:IR). apply eq_symmetric; apply Integral_empty. assumption. assert (Z:(Continuous_I Hab [-C-][0])). Contin. stepr (Integral Z). rstepl ([0][*](b[-]a)). apply eq_symmetric. apply Integral_const. apply Integral_wd. FEQ. simpl. simpl in Hx'. apply eq_symmetric. apply x_mult_zero. change ([0]:IR) with ([-C-][0] x I). apply Feq_imp_eq with (I:=Compact (less_leEq _ _ _ X1)); auto. apply Derivative_I_unique with G. eapply included_imp_deriv;[|apply HGG']. auto. apply Derivative_I_wdl with ([-C-](G a HGa)); [|apply Derivative_I_const]. FEQ. eapply included_trans. apply Habcd. eapply derivative_imp_inc. apply HGG'. rename H0 into X2. destruct HGF as [HGF0 HGF1]. simpl. apply leEq_imp_eq. apply leEq_transitive with d0. destruct (HGF1 _ HGa (compact_Min_lft _ _ Hab)); assumption. stepl c0; [| assumption]. destruct (HGF1 _ Hx'0 X2); assumption. apply leEq_transitive with d0. destruct (HGF1 _ Hx'0 X2); assumption. stepl c0; [| assumption]. destruct (HGF1 _ HGa (compact_Min_lft _ _ Hab)); assumption. assert (Hab':a[=]b). apply not_ap_imp_eq. intros X0. apply (eq_imp_not_ap _ _ _ X1). apply less_imp_ap. apply ap_imp_Min_less_Max. assumption. apply eq_transitive with ([0]:IR). apply Integral_empty. assumption. apply eq_symmetric. apply Integral_empty. algebra. Qed.
imports: CoRN.ftc.FTC CoRN.ftc.Composition