case zero
α : Type ?u.227526
β : Type ?u.227529
γ : Type ?u.227532
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ↑Nat.zero ≤ ord ↑Nat.zero

case succ
α : Type ?u.227526
β : Type ?u.227529
γ : Type ?u.227532
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
n : ℕ
IH : ↑n ≤ ord ↑n
⊢ ↑(Nat.succ n) ≤ ord ↑(Nat.succ n)
α : Type ?u.227526
β : Type ?u.227529
γ : Type ?u.227532
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
n : ℕ
⊢ ↑n ≤ ord ↑n
induction' n with n IH
no goals
case zero
α : Type ?u.227526
β : Type ?u.227529
γ : Type ?u.227532
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ↑Nat.zero ≤ ord ↑Nat.zero
apply Ordinal.zero_le
no goals
case succ
α : Type ?u.227526
β : Type ?u.227529
γ : Type ?u.227532
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
n : ℕ
IH : ↑n ≤ ord ↑n
⊢ ↑(Nat.succ n) ≤ ord ↑(Nat.succ n)
exact succ_le_of_lt (IH.trans_lt <| ord_lt_ord.2 <| natCast_lt.2 (Nat.lt_succ_self n))