proposition: Lemma le_mult_mult : forall a b c d:nat, a <= c -> b <= d -> a * b <= c * d.
proof: Proof. intros a b c d H H0. apply Nat.le_trans with (m := c * b). - apply mult_le_compat_r; assumption. - apply Nat.mul_le_mono_l; assumption. Qed.
imports: ZArith List Arith ZArithRing Relations Lia