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. eapply Nat.le_trans. - eapply Nat.mul_le_mono_l. eexact H0. - now apply mult_le_compat_r. Qed.
imports: ZArith List Arith ZArithRing Relations Lia