fact: Definition inject_Q (q : Q) : CReal := {| seq := (fun n : Z => q); scale := Qbound_ltabs_ZExp2 q; cauchy := inject_Q_cauchy q; bound := (fun _ : Z => Qbound_ltabs_ZExp2_spec q) |}.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra