fact: Record DedekindDecCut : Type := { DDupcut : Q -> Prop; DDproper : forall q r : Q, (q == r -> DDupcut q -> DDupcut r)%Q; DDlow : Q; DDhigh : Q; DDdec : forall q:Q, { DDupcut q } + { ~DDupcut q }; DDinterval : forall q r : Q, Qle q r -> DDupcut q -> DDupcut r; DDhighProp : DDupcut DDhigh; DDlowProp : ~DDupcut DDlow; }.
imports: QArith_base Qabs ConstructiveReals ConstructiveAbs ConstructiveLimits Logic.ConstructiveEpsilon