proposition: Lemma CReal_abs_gt : forall x : CReal, x < CReal_abs x -> x < 0.
proof: Proof. intros x [n nmaj]. unfold CReal_abs, CReal_abs_seq, CReal_abs_scale in nmaj; rewrite CReal_red_seq in nmaj. assert (seq x n < 0)%Q. { destruct (Qlt_le_dec (seq x n) 0) as [Hdec|Hdec]. - exact Hdec. - exfalso. rewrite Qabs_pos in nmaj by apply Hdec. pose proof Qpower_0_lt 2 n; lra. } rewrite Qabs_neg in nmaj by apply Qlt_le_weak, H. apply (CRealLt_RQ_from_single_dist _ _ n); lra. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra