proposition: Lemma CRinv_r : forall {R : ConstructiveReals} (r:CRcarrier R) (rnz : r ≶ 0), r * (/ r) rnz == 1.
proof: Proof. intros. transitivity ((/ r) rnz * r). - apply (CRisRing R). - apply CRinv_l. Qed.
imports: QArith Qabs Qround