proposition: Lemma CRlt_le_trans : forall {R : ConstructiveReals} (r1 r2 r3 : CRcarrier R), r1 < r2 -> r2 <= r3 -> r1 < r3.
proof: Proof. intros. destruct (CRltLinear R). destruct (s r1 r3 r2 H). - apply c. - contradiction. Qed.
imports: QArith Qabs Qround