proposition: Lemma CRealLt_lpo_dec : forall x y : CReal, (forall (P : nat -> Prop), (forall n:nat, {P n} + {~P n}) -> {n | ~P n} + {forall n, P n}) -> CRealLt x y + (CRealLt x y -> False).
proof: Proof. intros x y lpo. destruct (lpo (fun n:nat => seq y (Z_inj_nat_rev n) - seq x (Z_inj_nat_rev n) <= 2 * 2 ^ (Z_inj_nat_rev n) )). - intro n. destruct (Qlt_le_dec (2 * 2 ^ (Z_inj_nat_rev n)) (seq y (Z_inj_nat_rev n) - seq x (Z_inj_nat_rev n))). + right; lra. + left; lra. - left; destruct s as [n nmaj]; exists (Z_inj_nat_rev n); lra. - right; intro abs; destruct abs as [n majn]. specialize (q (Z_inj_nat n)). rewrite Z_inj_nat_id in q. pose proof (Qle_not_lt _ _ q). contradiction. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra