proposition: Lemma CRmult_1_r : forall {R : ConstructiveReals} (x : CRcarrier R), x * 1 == x.
proof: Proof. intros. destruct (CRisRing R). transitivity (CRmult R 1 x). - apply Rmul_comm. - apply Rmul_1_l. Qed.
imports: QArith Qabs Qround