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