α : Type ?u.129087
β : Type ?u.129090
γ : Type ?u.129093
δ : Type ?u.129096
σ : Type ?u.129099
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
p : ℕ × ℕ
⊢ Nat.rec true (fun n n_ih => false) (p.fst - p.snd) = decide (p.fst ≤ p.snd)
α : Type ?u.129087
β : Type ?u.129090
γ : Type ?u.129093
δ : Type ?u.129096
σ : Type ?u.129099
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
p : ℕ × ℕ
⊢ (Nat.casesOn ((fun x x_1 => x - x_1) p.fst p.snd) true fun b => false) =
    (fun a b => decide ((fun x x_1 => x ≤ x_1) a b)) p.fst p.snd
dsimp [swap]
case zero
α : Type ?u.129087
β : Type ?u.129090
γ : Type ?u.129093
δ : Type ?u.129096
σ : Type ?u.129099
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
p : ℕ × ℕ
e : p.fst - p.snd = Nat.zero
⊢ Nat.rec true (fun n n_ih => false) Nat.zero = decide (p.fst ≤ p.snd)

case succ
α : Type ?u.129087
β : Type ?u.129090
γ : Type ?u.129093
δ : Type ?u.129096
σ : Type ?u.129099
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
p : ℕ × ℕ
n : ℕ
e : p.fst - p.snd = Nat.succ n
⊢ Nat.rec true (fun n n_ih => false) (Nat.succ n) = decide (p.fst ≤ p.snd)
α : Type ?u.129087
β : Type ?u.129090
γ : Type ?u.129093
δ : Type ?u.129096
σ : Type ?u.129099
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
p : ℕ × ℕ
⊢ Nat.rec true (fun n n_ih => false) (p.fst - p.snd) = decide (p.fst ≤ p.snd)
cases' e : p.1 - p.2 with n
no goals
case zero
α : Type ?u.129087
β : Type ?u.129090
γ : Type ?u.129093
δ : Type ?u.129096
σ : Type ?u.129099
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
p : ℕ × ℕ
e : p.fst - p.snd = Nat.zero
⊢ Nat.rec true (fun n n_ih => false) Nat.zero = decide (p.fst ≤ p.snd)
simp [tsub_eq_zero_iff_le.1 e]
no goals
case succ
α : Type ?u.129087
β : Type ?u.129090
γ : Type ?u.129093
δ : Type ?u.129096
σ : Type ?u.129099
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
p : ℕ × ℕ
n : ℕ
e : p.fst - p.snd = Nat.succ n
⊢ Nat.rec true (fun n n_ih => false) (Nat.succ n) = decide (p.fst ≤ p.snd)
simp [not_le.2 (Nat.lt_of_sub_eq_succ e)]