proposition: Lemma CReq_trans : forall {R : ConstructiveReals} (x y z : CRcarrier R), x == y -> y == z -> x == z.
proof: Proof. intros. destruct H,H0. destruct (CRltLinear R), p. split. - intro abs. destruct (s _ y _ abs); contradiction. - intro abs. destruct (s _ y _ abs); contradiction. Qed.
imports: QArith Qabs Qround