proposition: Lemma CReal_le_abs : forall x : CReal, x <= CReal_abs x.
proof: Proof. intros x [n nmaj]. unfold CReal_abs, CReal_abs_seq, CReal_abs_scale in nmaj; rewrite CReal_red_seq in nmaj. apply (Qle_not_lt _ _ (Qle_Qabs (seq x n))). apply Qlt_minus_iff. apply (Qlt_trans _ (2*2^n)). - pose proof Qpower_0_lt 2 n ltac:(lra); lra. - exact nmaj. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra