proposition: Lemma CReal_abs_appart_0 : forall x : CReal, 0 < 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. destruct (Qlt_le_dec (seq x n) 0) as [Hdec|Hdec]. - left. exists n. cbn in nmaj |- * . rewrite Qabs_neg in nmaj; lra. - right. exists n. cbn. rewrite Qabs_pos in nmaj. + exact nmaj. + exact Hdec. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra