a : Ordinal
H : ∀ ⦃b c : Ordinal⦄, b < a → c < a → b + c ≠ a
ha : ¬Principal (fun x x_1 => x + x_1) a
⊢ False
a : Ordinal
H : ∀ ⦃b c : Ordinal⦄, b < a → c < a → b + c ≠ a
⊢ Principal (fun x x_1 => x + x_1) a
by_contra' ha
case intro.intro.intro.intro
b c : Ordinal
H : ∀ ⦃b_1 c_1 : Ordinal⦄, b_1 < b + c → c_1 < b + c → b_1 + c_1 ≠ b + c
ha : ¬Principal (fun x x_1 => x + x_1) (b + c)
hb : b < b + c
hc : c < b + c
⊢ False
a : Ordinal
H : ∀ ⦃b c : Ordinal⦄, b < a → c < a → b + c ≠ a
ha : ¬Principal (fun x x_1 => x + x_1) a
⊢ False
rcases exists_lt_add_of_not_principal_add ha with ⟨b, c, hb, hc, rfl⟩
no goals
case intro.intro.intro.intro
b c : Ordinal
H : ∀ ⦃b_1 c_1 : Ordinal⦄, b_1 < b + c → c_1 < b + c → b_1 + c_1 ≠ b + c
ha : ¬Principal (fun x x_1 => x + x_1) (b + c)
hb : b < b + c
hc : c < b + c
⊢ False
exact (H hb hc).irrefl