proposition: Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2.
proof: Proof. intros r r1 r2 Hr [I | E]. - now left; apply (Rmult_lt_reg_l r). - now apply Rlt_not_eq, not_eq_sym in Hr; right; apply (Rmult_eq_reg_l r). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField