proposition: Lemma CReal_plus_0_r : forall r : CReal, r + 0 == r.
proof: Proof. intro r. rewrite CReal_plus_comm. apply CReal_plus_0_l. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra