a : Ordinal
ha : ¬∀ ⦃a_1 b : Ordinal⦄, a_1 < a → b < a → (fun x x_1 => x + x_1) a_1 b < a
⊢ ∃ b c x x, b + c = a
a : Ordinal
ha : ¬Principal (fun x x_1 => x + x_1) a
⊢ ∃ b c x x, b + c = a
unfold Principal at ha
a : Ordinal
ha : Exists fun ⦃a_1⦄ => Exists fun ⦃b⦄ => a_1 < a ∧ b < a ∧ a ≤ a_1 + b
⊢ ∃ b c x x, b + c = a
a : Ordinal
ha : ¬∀ ⦃a_1 b : Ordinal⦄, a_1 < a → b < a → (fun x x_1 => x + x_1) a_1 b < a
⊢ ∃ b c x x, b + c = a
push_neg  at ha
case intro.intro.intro.intro
a b c : Ordinal
hb : b < a
hc : c < a
H : a ≤ b + c
⊢ ∃ b c x x, b + c = a
a : Ordinal
ha : Exists fun ⦃a_1⦄ => Exists fun ⦃b⦄ => a_1 < a ∧ b < a ∧ a ≤ a_1 + b
⊢ ∃ b c x x, b + c = a
rcases ha with ⟨b, c, hb, hc, H⟩
case intro.intro.intro.intro
a b c : Ordinal
hb : b < a
hc : c < a
H : a ≤ b + c
hab : a - b = a
⊢ False
case intro.intro.intro.intro
a b c : Ordinal
hb : b < a
hc : c < a
H : a ≤ b + c
⊢ ∃ b c x x, b + c = a
refine'
  ⟨b, _, hb, lt_of_le_of_ne (sub_le_self a b) fun hab => _, Ordinal.add_sub_cancel_of_le hb.le⟩
case intro.intro.intro.intro
a b c : Ordinal
hb : b < a
hc : c < a
H : a ≤ c
hab : a - b = a
⊢ False
case intro.intro.intro.intro
a b c : Ordinal
hb : b < a
hc : c < a
H : a ≤ b + c
hab : a - b = a
⊢ False
rw [← sub_le, hab] at H
no goals
case intro.intro.intro.intro
a b c : Ordinal
hb : b < a
hc : c < a
H : a ≤ c
hab : a - b = a
⊢ False
exact H.not_lt hc