no goals
α : Type ?u.84510
β : Type ?u.84513
γ : Type ?u.84516
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
⊢ pred o < o ↔ ¬pred o = o
simp only [le_antisymm_iff, pred_le_self, true_and_iff, not_le]