proposition: Lemma Rinv_eq_compat : forall x y (rxnz : x # 0) (rynz : y # 0), x == y -> (/ x) rxnz == (/ y) rynz.
proof: Proof. intros. apply (CReal_mult_eq_reg_l x). - exact rxnz. - rewrite CReal_inv_r, H, CReal_inv_r. reflexivity. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra