proposition: Lemma Rmult_le_compat_l : forall r r1 r2, 0 <= r -> r1 <= r2 -> r * r1 <= r * r2.
proof: Proof. intros r r1 r2 [I | <-] [I' | ->]; try rewrite 2Rmult_0_l; try apply Rle_refl. now left; apply Rmult_lt_compat_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField