proposition: Lemma max_plus : forall (a b c : IR), Max (a[+]c) (b[+]c) [=] Max a b [+] c.
proof: Proof. intros. apply equiv_imp_eq_max; intros. apply shift_plus_leEq. apply Max_leEq; apply shift_leEq_minus; auto. apply leEq_transitive with (Max a b [+]c); auto. apply plus_resp_leEq. apply lft_leEq_Max. apply leEq_transitive with (Max a b [+]c); auto. apply plus_resp_leEq. apply rht_leEq_Max. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq