proposition: Lemma CRlt_trans_flip : forall {R : ConstructiveReals} (x y z : CRcarrier R), y < z -> x < y -> x < z.
proof: Proof. intros. apply (CRlt_le_trans _ y). - exact H0. - apply CRlt_asym. exact H. Qed.
imports: QArith Qabs Qround