proposition: Lemma inject_Q_one : inject_Q 1 == 1.
proof: Proof. split. all: intros [n nmaj]; cbn in nmaj. all: assert(2^n>0)%Q by (apply Qpower_0_lt; lra); lra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra