proposition: Lemma CReal_plus_eq_reg_l : forall (r r1 r2 : CReal), r + r1 == r + r2 -> r1 == r2.
proof: Proof. intros. destruct H. split. - intro abs. apply (CReal_plus_lt_compat_l r) in abs. contradiction. - intro abs. apply (CReal_plus_lt_compat_l r) in abs. contradiction. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra