no goals
α : Type ?u.137547
β : Type ?u.137550
γ : Type ?u.137553
δ : Type ?u.137556
σ : Type ?u.137559
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
p : ℕ × ℕ
⊢ ¬p.snd ≤ p.fst ↔ (fun x x_1 => x < x_1) p.fst p.snd
simp