proposition: Lemma CRealLt_asym : forall x y : CReal, x < y -> x <= y.
proof: Proof. intros x y H [n q]. apply CRealLt_above in H. destruct H as [p H]. pose proof (CRealLt_above_same y x n q). apply (Qlt_not_le (seq y (Z.min n p)) (seq x (Z.min n p))). - apply H0. apply Z.le_min_l. - apply Qlt_le_weak. apply (Qplus_lt_l _ _ (-seq x (Z.min n p))). rewrite Qplus_opp_r. apply (Qlt_trans _ (2*2^p)). + pose proof Qpower_0_lt 2 p ltac:(lra). lra. + apply H. lia. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra