proposition: Lemma DDlow_below_up : forall (upcut : DedekindDecCut) (a b : Q), DDupcut upcut a -> ~DDupcut upcut b -> Qlt b a.
proof: Proof. intros. destruct (Qlt_le_dec b a). - exact q. - exfalso. apply H0. apply (DDinterval upcut a). + exact q. + exact H. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveAbs ConstructiveLimits Logic.ConstructiveEpsilon