proposition: Lemma Rinv_1_lt_contravar : forall r1 r2, 1 <= r1 -> r1 < r2 -> / r2 < / r1.
proof: Proof. intros r1 r2 H1 I. apply Rlt_le_trans with (1 := Rlt_0_1) in H1. now apply Rinv_0_lt_contravar. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField