proposition: Lemma Rmult_lt_reg_r : forall r r1 r2 : R, 0 < r -> r1 * r < r2 * r -> r1 < r2.
proof: Proof. intros r r1 r2 H I; apply (Rmult_lt_reg_l r); try easy. now rewrite 2(Rmult_comm r). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField