case h.e'_3
a b : Cardinal
h : b ≠ 0
⊢ a = 1 * a
a b : Cardinal
h : b ≠ 0
⊢ a ≤ b * a
convert mul_le_mul_right' (one_le_iff_ne_zero.mpr h) a
no goals
case h.e'_3
a b : Cardinal
h : b ≠ 0
⊢ a = 1 * a
rw [one_mul]