proposition: Lemma Rinv_inv r : / / r = r.
proof: Proof. destruct (Req_dec r 0) as [-> | H]. - now rewrite Rinv_0, Rinv_0. - symmetry; apply Rmult_inv_r_uniq. * now apply Rinv_neq_0_compat. * now rewrite Rinv_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField