a b c : Ordinal
⊢ a < max (blsub b fun a' x => a' ♯ c) (blsub c fun b' x => b ♯ b') ↔
    (∃ b', b' < b ∧ a ≤ b' ♯ c) ∨ ∃ c', c' < c ∧ a ≤ b ♯ c'
a b c : Ordinal
⊢ a < b ♯ c ↔ (∃ b', b' < b ∧ a ≤ b' ♯ c) ∨ ∃ c', c' < c ∧ a ≤ b ♯ c'
rw [nadd_def]
no goals
a b c : Ordinal
⊢ a < max (blsub b fun a' x => a' ♯ c) (blsub c fun b' x => b ♯ b') ↔
    (∃ b', b' < b ∧ a ≤ b' ♯ c) ∨ ∃ c', c' < c ∧ a ≤ b ♯ c'
simp [lt_blsub_iff]