proposition: Lemma inject_Q_cauchy : forall q : Q, QCauchySeq (fun _ => q).
proof: Proof. intros q k p r Hp Hr. apply Qabs_Qlt_condition. pose proof Qpower_0_lt 2 k; lra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra