no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
⊢ 0 < 2
decide
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
⊢ 1 < 2
decide
case zero
α : Type u
β : Type v
inst✝ : DecidableEq α
hn : 2 ≤ Nat.zero
⊢ signAux (swap { val := 0, isLt := (_ : 0 < Nat.zero) } { val := 1, isLt := (_ : 1 < Nat.zero) }) = -1

case succ.zero
α : Type u
β : Type v
inst✝ : DecidableEq α
hn : 2 ≤ Nat.succ Nat.zero
⊢ signAux (swap { val := 0, isLt := (_ : 0 < Nat.succ Nat.zero) } { val := 1, isLt := (_ : 1 < Nat.succ Nat.zero) }) =
    -1

case succ.succ
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ Nat.succ (Nat.succ n)
⊢ signAux
      (swap { val := 0, isLt := (_ : 0 < Nat.succ (Nat.succ n)) }
        { val := 1, isLt := (_ : 1 < Nat.succ (Nat.succ n)) }) =
    -1
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
⊢ signAux (swap { val := 0, isLt := (_ : 0 < n) } { val := 1, isLt := (_ : 1 < n) }) = -1
rcases n with (_ | _ | n)
no goals
case zero
α : Type u
β : Type v
inst✝ : DecidableEq α
hn : 2 ≤ Nat.zero
⊢ signAux (swap { val := 0, isLt := (_ : 0 < Nat.zero) } { val := 1, isLt := (_ : 1 < Nat.zero) }) = -1
norm_num at hn
no goals
case succ.zero
α : Type u
β : Type v
inst✝ : DecidableEq α
hn : 2 ≤ Nat.succ Nat.zero
⊢ signAux (swap { val := 0, isLt := (_ : 0 < Nat.succ Nat.zero) } { val := 1, isLt := (_ : 1 < Nat.succ Nat.zero) }) =
    -1
norm_num at hn
no goals
case succ.succ
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ Nat.succ (Nat.succ n)
⊢ signAux
      (swap { val := 0, isLt := (_ : 0 < Nat.succ (Nat.succ n)) }
        { val := 1, isLt := (_ : 1 < Nat.succ (Nat.succ n)) }) =
    -1
exact signAux_swap_zero_one' n