proposition: Lemma Rinv_opp r : / - r = - / r.
proof: Proof. destruct (Req_dec r 0) as [-> | H]. - now rewrite Ropp_0, Rinv_0, Ropp_0. - symmetry; apply Rmult_inv_r_uniq. { now apply Ropp_neq_0_compat. } now rewrite Rmult_opp_opp, Rinv_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField