proposition: Lemma Rbar_inv_opp (x : Rbar) : x <> 0 -> Rbar_inv (Rbar_opp x) = Rbar_opp (Rbar_inv x).
proof: Proof. case: x => [x | | ] /= Hx. rewrite Ropp_inv_permute => //. contradict Hx. by rewrite Hx. by rewrite Ropp_0. by rewrite Ropp_0. Qed.
imports: Coq(Reals ssreflect) Rcomplements