proposition: Lemma Max_leEq : forall x y z : IR, x [<=] z -> y [<=] z -> Max x y [<=] z.
proof: Proof. unfold Max in |- *. simpl in |- *. intros. rewrite -> leEq_def in |- *. intro H1. generalize (less_MAX_imp _ _ _ H1); intro H2. elim H2; intros. rewrite -> leEq_def in H; elim H. assumption. rewrite -> leEq_def in H0; elim H0. assumption. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq