proposition: Lemma CReal_abs_le : forall a b:CReal, -b <= a <= b -> CReal_abs a <= b.
proof: Proof. intros a b H [n nmaj]. unfold CReal_abs, CReal_abs_seq, CReal_abs_scale in nmaj; rewrite CReal_red_seq in nmaj. destruct (Qlt_le_dec (seq a n) 0) as [Hdec|Hdec]. - rewrite Qabs_neg in nmaj by lra. destruct H as [Hl Hr]. apply Hl. clear Hl Hr. exists n; cbn. unfold CReal_opp_seq; lra. - rewrite Qabs_pos in nmaj. + destruct H as [Hl Hr]. apply Hr. clear Hl Hr. exists n; cbn. exact nmaj. + exact Hdec. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra