proposition: Lemma CR_of_Q_le : forall {R : ConstructiveReals} (r q : Q), Qle r q -> CR_of_Q R r <= CR_of_Q R q.
proof: Proof. intros. intro abs. apply lt_CR_of_Q in abs. exact (Qlt_not_le _ _ abs H). Qed.
imports: QArith Qabs Qround