no goals
α : Type ?u.224685
β : Type ?u.224688
γ : Type ?u.224691
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≠ 0
⊢ succ a ≤ b * succ a
simpa only [succ_zero, one_mul] using
  mul_le_mul_right' (succ_le_of_lt (Ordinal.pos_iff_ne_zero.2 h)) (succ a)