no goals
α : Type ?u.75944
β : Type ?u.75947
γ : Type ?u.75950
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
⊢ a + ↑0 ≤ b + ↑0 ↔ a ≤ b
simp
no goals
α : Type ?u.75944
β : Type ?u.75947
γ : Type ?u.75950
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
n : ℕ
⊢ a + ↑(n + 1) ≤ b + ↑(n + 1) ↔ a ≤ b
simp only [nat_cast_succ, add_succ, add_succ, succ_le_succ_iff, add_le_add_iff_right]