proposition: Lemma Max_wd_unfolded : forall x y x' y', x [=] x' -> y [=] y' -> Max x y [=] Max x' y'.
proof: Proof. cut (bin_op_wd _ MAX); [ intro | apply MAX_wd ]. red in H. red in H. intros; apply H; assumption. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq