proposition: Lemma CRealEq_trans : forall x y z : CReal, CRealEq x y -> CRealEq y z -> CRealEq x z.
proof: Proof. intros x y z Hxeqy Hyeqz. destruct Hxeqy as [Hylex Hxley]. destruct Hyeqz as [Hzley Hylez]. split. - intro contra. destruct (CRealLt_dec _ _ y contra); contradiction. - intro contra. destruct (CRealLt_dec _ _ y contra); contradiction. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra