proposition: Lemma CRealLt_dec : forall x y z : CReal, x < y -> sum (x < z) (z < y).
proof: Proof. intros x y z [n inf]. destruct (QarchimedeanExp2_Z (/((seq y) n - (seq x) n - (2 * 2 ^ n)))) as [k kmaj]. rewrite Qinv_lt_contravar, Qinv_involutive, <- Qpower_opp in kmaj. 3: apply Qpower_0_lt; lra. 2: apply Qinv_lt_0_compat; lra. destruct (Qlt_le_dec ((1#2) * ((seq y) n + (seq x) n)) ((seq z) (Z.min n (- k - 2)))) as [Hxyltz|Hzlexy]; [left; pose (cauchy x) as HCS|right; pose (cauchy y) as HCS]. all: exists (Z.min (n)%Z (-k - 2))%Z. all: specialize (HCS n n (Z.min n (-k-2))%Z ltac:(lia) ltac:(lia)). all: rewrite Qabs_Qlt_condition in HCS. all: assert (2 ^ Z.min n (- k - 2) <= 2 ^ (- k - 2))%Q as Hpowmin by (apply Qpower_le_compat_l; [lia|lra]). all: rewrite Qpower_minus_pos in Hpowmin; lra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra