proposition: Lemma Integral_ap_zero : forall a b Hab (F : PartIR) contF, a [#] b -> forall x, Compact Hab x -> forall Hx, [0] [<] F x Hx -> (forall x, Compact Hab x -> forall Hx, [0] [<=] F x Hx) -> [0] [<] AbsIR (Integral (a:=a) (b:=b) (Hab:=Hab) (F:=F) contF).
proof: Proof. intros a b Hab F contF H x H0 Hx H1 H2. elim (ap_imp_less _ _ _ H); intro. eapply less_leEq_trans. 2: apply leEq_AbsIR. eapply less_wdr. 2: apply eq_symmetric_unfolded. 2: apply Integral_integral with (HF' := included_imp_contin _ _ _ _ _ _ _ (compact_map2 a b (less_leEq _ _ _ a0) Hab) contF). eapply integral_gt_zero with x Hx; auto. exact (compact_map1 _ _ (less_leEq _ _ _ a0) Hab x H0). intros x0 H3 Hx0; apply H2. exact (compact_map2 _ _ (less_leEq _ _ _ a0) Hab _ H3). cut (included (Compact (Min_leEq_Max b a)) (Compact Hab)). 2: apply included_compact; split. 2: apply eq_imp_leEq; apply Min_comm. 2: apply leEq_transitive with a; [ apply Min_leEq_rht | apply lft_leEq_Max ]. 2: apply leEq_transitive with b; [ apply Min_leEq_rht | apply lft_leEq_Max ]. 2: apply eq_imp_leEq; apply Max_comm. cut (included (Compact Hab) (Compact (Min_leEq_Max b a))). 2: apply included_compact; split. 2: apply eq_imp_leEq; apply Min_comm. 2: apply leEq_transitive with b; [ apply Min_leEq_rht | apply lft_leEq_Max ]. 2: apply leEq_transitive with a; [ apply Min_leEq_rht | apply lft_leEq_Max ]. 2: apply eq_imp_leEq; apply Max_comm. intros H3 H4. eapply less_leEq_trans. 2: apply inv_leEq_AbsIR. eapply less_wdr. 2: apply Integral_op with (contF := included_imp_contin _ _ _ _ _ _ _ H4 contF). eapply less_wdr. 2: apply eq_symmetric_unfolded. 2: apply Integral_integral with (HF' := included_imp_contin _ _ _ _ _ _ _ (compact_map2 _ _ (less_leEq _ _ _ b0) (Min_leEq_Max b a)) (included_imp_contin _ _ _ _ _ _ _ H4 contF)). eapply integral_gt_zero with x Hx; auto. exact (compact_map1 _ _ (less_leEq _ _ _ b0) (Min_leEq_Max b a) x (H3 x H0)). intros x0 H5 Hx0; apply H2. exact (H4 _ (compact_map2 _ _ (less_leEq _ _ _ b0) (Min_leEq_Max _ _) _ H5)). Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions