proposition: Lemma opp_inject_Q : forall q : Q, inject_Q (-q) == - inject_Q q.
proof: Proof. intros q. split. all: intros [n maj]; cbn in maj. all: unfold CReal_opp_seq, inject_Q in maj. all: rewrite CReal_red_seq in maj. 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