fact: Fixpoint DDcut_limit_fix (upcut : DedekindDecCut) (r : Q) (n : nat) : Qlt 0 r -> (DDupcut upcut (DDlow upcut + (Z.of_nat n#1) * r)) -> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (q - r) }.
imports: QArith_base Qabs ConstructiveReals ConstructiveAbs ConstructiveLimits Logic.ConstructiveEpsilon