no goals
a b : Cardinal
ha : ℵ₀ ≤ a
hb : ℵ₀ ≤ b
⊢ a ≤ a * b
simpa only [mul_one] using mul_le_mul_left' (one_le_aleph0.trans hb) a
no goals
a b : Cardinal
ha : ℵ₀ ≤ a
hb : ℵ₀ ≤ b
⊢ b ≤ a * b
simpa only [one_mul] using mul_le_mul_right' (one_le_aleph0.trans ha) b