proposition: Lemma FMin_char : forall x Hx Hx' Hx'', FMin x Hx [=] Min (F x Hx') (G x Hx'').
proof: Proof. intros. Opaque Max. simpl in |- *; unfold MIN; algebra. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq