proposition: Lemma CRinv_morph : forall {R : ConstructiveReals} (x y : CRcarrier R) (rxnz : x ≶ 0) (rynz : y ≶ 0), x == y -> (/ x) rxnz == (/ y) rynz.
proof: Proof. intros. apply (CRmult_eq_reg_l x). - exact rxnz. - rewrite CRinv_r, H, CRinv_r. reflexivity. Qed.
imports: QArith Qabs Qround