proposition: Lemma CRzero_double : forall {R : ConstructiveReals} (x : CRcarrier R), x == x + x -> x == 0.
proof: Proof. intros. apply (CRplus_eq_reg_l x), CReq_sym. transitivity x. - apply CRplus_0_r. - exact H. Qed.
imports: QArith Qabs Qround