proposition: Lemma integral_gt_zero : forall a b Hab (F : PartIR) contF, let N := Norm_Funct contF in 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] [<] integral a b Hab F contF.
proof: Proof. intros a b Hab F contF N Hless x H Hx H0. set (e := F x Hx [/]TwoNZ) in *. cut ([0] [<] e). intros H1 H2. 2: unfold e in |- *; apply pos_div_two; auto. elim (contin_prop _ _ _ _ contF e); auto. intros d H3 H4. set (mid1 := Max a (x[-]d)) in *. set (mid2 := Min b (x[+]d)) in *. cut (a [<=] mid1); [ intro leEq1 | unfold mid1 in |- *; apply lft_leEq_Max ]. cut (mid1 [<=] mid2); [ intro leEq2 | unfold mid1, mid2 in |- *; inversion_clear H; apply leEq_transitive with x ]. 2: apply Max_leEq; auto. 2: apply less_leEq; apply shift_minus_less. 2: apply shift_less_plus'; astepl ZeroR; auto. 2: apply leEq_Min; auto. 2: apply less_leEq; apply shift_less_plus'. 2: astepl ZeroR; auto. cut (mid2 [<=] b); [ intro leEq3 | unfold mid2 in |- *; apply Min_leEq_lft ]. cut (Continuous_I leEq1 F). cut (Continuous_I leEq2 F). cut (Continuous_I leEq3 F). intros cont3 cont2 cont1. cut (Continuous_I (leEq_transitive _ _ _ _ leEq1 leEq2) F). intro H5. apply less_wdr with (integral _ _ _ _ cont1[+]integral _ _ _ _ cont2[+]integral _ _ _ _ cont3). 2: apply eq_transitive_unfolded with (integral _ _ _ _ H5[+]integral _ _ _ _ cont3). 2: apply bin_op_wd_unfolded. 2: apply integral_plus_integral. 2: algebra. 2: apply integral_plus_integral. rstepl ([0][*] (mid1[-]a) [+][0][*] (mid2[-]mid1) [+][0][*] (b[-]mid2)). apply plus_resp_less_leEq. apply plus_resp_leEq_less. apply lb_integral. intros x0 H6 Hx0. apply H2. inversion_clear H6; split; auto. apply leEq_transitive with mid1; auto. apply leEq_transitive with mid2; auto. apply less_leEq_trans with (F x Hx [/]TwoNZ[*] (mid2[-]mid1)). apply mult_resp_less. apply pos_div_two; auto. apply shift_less_minus; astepl mid1. elim (less_cotransitive_unfolded _ _ _ Hless x); intro; unfold mid1, mid2 in |- *. apply less_leEq_trans with x. apply Max_less. auto. apply shift_minus_less; apply shift_less_plus'. astepl ZeroR; auto. apply leEq_Min. inversion_clear H; auto. apply less_leEq; apply shift_less_plus'. astepl ZeroR; auto. apply leEq_less_trans with x. apply Max_leEq. inversion_clear H; auto. apply shift_minus_leEq; apply shift_leEq_plus'. astepl ZeroR; apply less_leEq; auto. apply less_Min. auto. apply shift_less_plus'. astepl ZeroR; auto. apply lb_integral. intros x0 H6 Hx0. rstepl (F x Hx[-]F x Hx [/]TwoNZ). apply shift_minus_leEq; apply shift_leEq_plus'. fold e in |- *; eapply leEq_transitive; [ apply leEq_AbsIR | apply H4 ]. auto. inversion_clear H6; split; auto. apply leEq_transitive with mid1; auto. apply leEq_transitive with mid2; auto. cut (x[-]d [<=] x[+]d); intros. apply compact_bnd_AbsIR with H7. cut (included (Compact leEq2) (Compact H7)); auto. apply included_compact; unfold mid1, mid2 in |- *; split. apply rht_leEq_Max. apply leEq_transitive with mid2; auto. unfold mid2 in |- *; apply Min_leEq_rht. apply leEq_transitive with mid1; auto. unfold mid1 in |- *; apply rht_leEq_Max. apply Min_leEq_rht. apply leEq_transitive with x. apply shift_minus_leEq; apply shift_leEq_plus'. astepl ZeroR; apply less_leEq; auto. apply shift_leEq_plus'. astepl ZeroR; apply less_leEq; auto. apply lb_integral. intros x0 H6 Hx0. apply H2. inversion_clear H6; split; auto. apply leEq_transitive with mid1; auto. apply leEq_transitive with mid2; auto. apply included_imp_contin with a b Hab; auto. apply included_compact. apply compact_inc_lft. split; auto. apply leEq_transitive with mid1; auto. apply included_imp_contin with a b Hab; auto. apply included_compact. split; auto. apply leEq_transitive with mid1; auto. apply compact_inc_rht. apply included_imp_contin with a b Hab; auto. apply included_compact. split; auto. apply leEq_transitive with mid2; auto. split; auto. apply leEq_transitive with mid1; auto. apply included_imp_contin with a b Hab; auto. apply included_compact. apply compact_inc_lft. split; auto. apply leEq_transitive with mid2; auto. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)