proposition: Lemma Min_id : forall x : IR, Min x x [=] x.
proof: Proof. intro. simpl; unfold MIN. astepr ( [--][--]x). apply un_op_wd_unfolded; apply Max_id. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq