a b c : Ordinal
hb : 0 < b
h : ∀ (d : Ordinal), d < b → a + d < c
H : a + (c - a) = c
⊢ a + b ≤ c
a b c : Ordinal
hb : 0 < b
h : ∀ (d : Ordinal), d < b → a + d < c
⊢ a + b ≤ c
have H : a + (c - a) = c :=
  Ordinal.add_sub_cancel_of_le
    (by
      rw [← add_zero a]
      exact (h _ hb).le)
a b c : Ordinal
hb : 0 < b
h : ∀ (d : Ordinal), d < b → a + d < c
H : a + (c - a) = c
⊢ a + b ≤ a + (c - a)
a b c : Ordinal
hb : 0 < b
h : ∀ (d : Ordinal), d < b → a + d < c
H : a + (c - a) = c
⊢ a + b ≤ c
rw [← H]
a b c : Ordinal
hb : 0 < b
h : ∀ (d : Ordinal), d < b → a + d < c
H : a + (c - a) = c
⊢ b ≤ c - a
a b c : Ordinal
hb : 0 < b
h : ∀ (d : Ordinal), d < b → a + d < c
H : a + (c - a) = c
⊢ a + b ≤ a + (c - a)
apply add_le_add_left _ a
a b c : Ordinal
hb✝ : 0 < b
h : ∀ (d : Ordinal), d < b → a + d < c
H : a + (c - a) = c
hb : c - a < b
⊢ False
a b c : Ordinal
hb : 0 < b
h : ∀ (d : Ordinal), d < b → a + d < c
H : a + (c - a) = c
⊢ b ≤ c - a
by_contra' hb
no goals
a b c : Ordinal
hb✝ : 0 < b
h : ∀ (d : Ordinal), d < b → a + d < c
H : a + (c - a) = c
hb : c - a < b
⊢ False
exact (h _ hb).ne H
a b c : Ordinal
hb : 0 < b
h : ∀ (d : Ordinal), d < b → a + d < c
⊢ a + 0 ≤ c
a b c : Ordinal
hb : 0 < b
h : ∀ (d : Ordinal), d < b → a + d < c
⊢ a ≤ c
rw [← add_zero a]
no goals
a b c : Ordinal
hb : 0 < b
h : ∀ (d : Ordinal), d < b → a + d < c
⊢ a + 0 ≤ c
exact (h _ hb).le