α : Type ?u.236919
β : Type ?u.236922
γ : Type ?u.236925
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
n : ℕ
⊢ ↑(Nat.succ n) ≤ o ↔ succ ↑n ≤ o
α : Type ?u.236919
β : Type ?u.236922
γ : Type ?u.236925
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
n : ℕ
⊢ ↑n < card o ↔ ↑n < o
rw [← succ_le_iff, ← succ_le_iff, ← nat_succ, nat_le_card]
no goals
α : Type ?u.236919
β : Type ?u.236922
γ : Type ?u.236925
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
n : ℕ
⊢ ↑(Nat.succ n) ≤ o ↔ succ ↑n ≤ o
rfl