proposition: Lemma inject_Q_plus : forall q r : Q, inject_Q (q + r) == inject_Q q + inject_Q r.
proof: Proof. intros q r. split. all: intros [n nmaj]; unfold CReal_plus, CReal_plus_seq, inject_Q in nmaj. all: do 4 rewrite CReal_red_seq in nmaj. all: rewrite Qred_correct 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