proposition: Lemma CReal_abs_Qabs_seq: forall (x : CReal) (n : Z), (seq (CReal_abs x) n == Qabs (seq x n))%Q.
proof: Proof. intros x n. unfold CReal_abs, CReal_abs_seq; rewrite CReal_red_seq. reflexivity. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra Qminmax