proposition: Lemma CRmult_0_r : forall {R : ConstructiveReals} (x : CRcarrier R), x * 0 == 0.
proof: Proof. intros. apply CRzero_double. transitivity (x * (0 + 0)). - destruct (CRisRingExt R). apply Rmul_ext. + apply CReq_refl. + apply CReq_sym, CRplus_0_r. - destruct (CRisRing R). apply CRmult_plus_distr_l. Qed.
imports: QArith Qabs Qround