proposition: Lemma DDcut_limit : forall (upcut : DedekindDecCut) (r : Q), Qlt 0 r -> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (q - r) }.
proof: Proof. intros. destruct (Qarchimedean ((DDhigh upcut - DDlow upcut)/r)) as [n nmaj]. apply (DDcut_limit_fix upcut r (Pos.to_nat n) H). apply (Qmult_lt_r _ _ r) in nmaj. 2: exact H. unfold Qdiv in nmaj. rewrite <- Qmult_assoc, (Qmult_comm (/r)), Qmult_inv_r, Qmult_1_r in nmaj. - apply (DDinterval upcut (DDhigh upcut)). 2: exact (DDhighProp upcut). apply Qlt_le_weak. apply (Qplus_lt_r _ _ (-DDlow upcut)). rewrite Qplus_assoc, <- (Qplus_comm (DDlow upcut)), Qplus_opp_r, Qplus_0_l, Qplus_comm. rewrite positive_nat_Z. exact nmaj. - intros abs. rewrite abs in H. exact (Qlt_irrefl 0 H). Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveAbs ConstructiveLimits Logic.ConstructiveEpsilon