proposition: Lemma CRealLtEpsilon : forall x y : CReal, CRealLtProp x y -> x < y.
proof: Proof. intros x y H. unfold CRealLtProp in H. apply constructive_indefinite_ground_description_Z in H. - apply H. - intros n. pose proof Qlt_le_dec (2 * 2 ^ n) (seq y n - seq x n) as Hdec. destruct Hdec as [H1|H1]. + left; exact H1. + right; apply Qle_not_lt in H1; exact H1. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra