case inl
a✝ b c : Ordinal
h✝ : b ≤ c
a : Ordinal
h : b < c
⊢ b ♯ a ≤ c ♯ a

case inr
a✝ b a : Ordinal
h : b ≤ b
⊢ b ♯ a ≤ b ♯ a
a✝ b c : Ordinal
h : b ≤ c
a : Ordinal
⊢ b ♯ a ≤ c ♯ a
rcases lt_or_eq_of_le h with (h | rfl)
no goals
case inl
a✝ b c : Ordinal
h✝ : b ≤ c
a : Ordinal
h : b < c
⊢ b ♯ a ≤ c ♯ a
exact (nadd_lt_nadd_right h a).le
no goals
case inr
a✝ b a : Ordinal
h : b ≤ b
⊢ b ♯ a ≤ b ♯ a
exact le_rfl