proposition: Lemma mult_le_compat_r : forall m n p:nat, le n p -> le (n * m) (p * m).
proof: Proof. intros m n p H; rewrite (Nat.mul_comm n m); rewrite (Nat.mul_comm p m). apply Nat.mul_le_mono_l; trivial. Qed.
imports: ZArith List Arith ZArithRing Relations Lia