proposition: Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
proof: Proof. intros r r1 r2 Hr I%(Rmult_lt_compat_l (/ r)); try now apply Rinv_0_lt_compat. rewrite <-2(Rmult_assoc (/ r)), Rinv_l, 2Rmult_1_l in I; try easy. now apply not_eq_sym, Rlt_not_eq. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField