α : Type ?u.81368
β : Type ?u.81371
γ : Type ?u.81374
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : ∃ a, o = succ a
a : Ordinal
e : o = succ a
⊢ pred o ≤ o
α : Type ?u.81368
β : Type ?u.81371
γ : Type ?u.81374
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : ∃ a, o = succ a
⊢ pred o ≤ o
let ⟨a, e⟩ := h
α : Type ?u.81368
β : Type ?u.81371
γ : Type ?u.81374
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : ∃ a, o = succ a
a : Ordinal
e : o = succ a
⊢ a ≤ succ a
α : Type ?u.81368
β : Type ?u.81371
γ : Type ?u.81374
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : ∃ a, o = succ a
a : Ordinal
e : o = succ a
⊢ pred o ≤ o
rw [e, pred_succ]
no goals
α : Type ?u.81368
β : Type ?u.81371
γ : Type ?u.81374
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : ∃ a, o = succ a
a : Ordinal
e : o = succ a
⊢ a ≤ succ a
exact le_succ a
no goals
α : Type ?u.81368
β : Type ?u.81371
γ : Type ?u.81374
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : ¬∃ a, o = succ a
⊢ pred o ≤ o
rw [pred, dif_neg h]