no goals
a✝ b✝ : Cardinal
n m : ℕ
a x : Cardinal
b0 : x ≠ 0
b : Cardinal
hab : x = a * b
⊢ a ≤ x
simpa only [hab, mul_one] using
  mul_le_mul_left' (one_le_iff_ne_zero.2 fun h : b = 0 => b0 (by rwa [h, mul_zero] at hab)) a
no goals
a✝ b✝ : Cardinal
n m : ℕ
a x : Cardinal
b0 : x ≠ 0
b : Cardinal
hab : x = a * b
h : b = 0
⊢ x = 0
rwa [h, mul_zero] at hab