proposition: Lemma MIN_strext : bin_op_strext _ MIN.
proof: Proof. intros x1 x2 y1 y2 H. unfold MIN in H. assert (H':=(un_op_strext_unfolded _ _ _ _ H)). elim (bin_op_strext_unfolded _ _ _ _ _ _ H'); intro H1; [left | right]; exact (un_op_strext_unfolded _ _ _ _ H1). Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq