proposition: Lemma Abs_Max : forall a b : IR, AbsIR (a[-]b) [=] Max a b[-]Min a b.
proof: Proof. intros. apply leEq_imp_eq. apply leEq_wdl with (Max (a[-]b) (b[-]a)). 2: simpl in |- *; unfold ABSIR in |- *. 2: apply Max_wd_unfolded; rational. apply Max_leEq. unfold cg_minus in |- *; apply plus_resp_leEq_both. apply lft_leEq_Max. apply inv_resp_leEq; apply Min_leEq_rht. unfold cg_minus in |- *; apply plus_resp_leEq_both. apply rht_leEq_Max. apply inv_resp_leEq; apply Min_leEq_lft. astepr ([0][+]AbsIR (a[-]b)). apply shift_leEq_plus. apply approach_zero_weak. intros. do 2 apply shift_minus_leEq. eapply leEq_wdr. 2: apply CSemiGroups.plus_assoc. apply shift_leEq_plus'. rename X into H. elim (Max_minus_eps_leEq a b e H); intro. apply leEq_transitive with a. assumption. apply shift_leEq_plus'. apply leEq_Min. apply shift_minus_leEq; apply shift_leEq_plus'. astepl ZeroR; apply AbsIR_nonneg. apply shift_minus_leEq; apply shift_leEq_plus'. apply leEq_AbsIR. apply leEq_transitive with b. assumption. apply shift_leEq_plus'. apply leEq_Min. apply shift_minus_leEq; apply shift_leEq_plus'. rstepl ( [--] (a[-]b)); apply inv_leEq_AbsIR. apply shift_minus_leEq; apply shift_leEq_plus'. astepl ZeroR; apply AbsIR_nonneg. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq