proposition: Lemma Rinv_lt_0_compat : forall r, r < 0 -> / r < 0.
proof: Proof. intros r H%Ropp_lt_contravar; apply Ropp_lt_cancel. now rewrite Ropp_0 in H |- *; rewrite <-Rinv_opp; apply Rinv_0_lt_compat. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField