proposition: Lemma Integral_leEq_norm : AbsIR (Integral contF) [<=] Norm_Funct contF[*]AbsIR (b[-]a).
proof: Proof. unfold Integral in |- *. eapply leEq_transitive. apply triangle_IR_minus. apply leEq_transitive with (Norm_Funct contF[*] (b[-]Min a b) [+]Norm_Funct contF[*] (a[-]Min a b)). apply plus_resp_leEq_both; (eapply leEq_transitive; [ apply integral_leEq_norm | apply mult_resp_leEq_rht ]). apply leEq_Norm_Funct; intros. apply norm_bnd_AbsIR; apply compact_inc_Min_rht with (H := Min_leEq_rht a b); assumption. apply shift_leEq_minus; astepl (Min a b); apply Min_leEq_rht. apply leEq_Norm_Funct; intros. apply norm_bnd_AbsIR; apply compact_inc_Min_lft with (H := Min_leEq_lft a b); assumption. apply shift_leEq_minus; astepl (Min a b); apply Min_leEq_lft. eapply leEq_wdl. 2: apply ring_dist_unfolded. apply mult_resp_leEq_lft. 2: apply positive_norm. rstepl (a[+]b[-]Two[*]Min a b). apply shift_minus_leEq; apply shift_leEq_plus'. apply shift_leEq_mult' with (two_ap_zero IR). apply pos_two. apply leEq_Min. apply shift_div_leEq. apply pos_two. apply shift_minus_leEq; apply shift_leEq_plus'. rstepl (b[-]a); apply leEq_AbsIR. apply shift_div_leEq. apply pos_two. apply shift_minus_leEq; apply shift_leEq_plus'. rstepl ( [--] (b[-]a)); apply inv_leEq_AbsIR. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions