proposition: Lemma Rinv_0_lt_compat : forall r, 0 < r -> 0 < / r.
proof: Proof. intros r Hr. destruct (Rlt_or_le 0 (/ r)) as [Hlt | Hle]; try easy. exfalso; apply (Rle_not_lt 0 1); try apply Rlt_0_1. rewrite <-(Rinv_l r), <-(Rmult_0_r (/ r)); cycle 1. { now apply not_eq_sym, Rlt_not_eq. } now apply Rlt_le in Hr; apply Rmult_le_compat_neg_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField