no goals
x : Nat
xs : List Nat
⊢ insert x xs ≠ []
induction xs with
| nil => simp [insert]
| cons x xs _  => simp [insert]; split <;> simp
no goals
case nil
x : Nat
⊢ insert x [] ≠ []
simp [insert]
case cons
x✝ x : Nat
xs : List Nat
tail_ih✝ : insert x✝ xs ≠ []
⊢ ¬(if x✝ < x then x✝ :: x :: xs else x :: insert x✝ xs) = []
case cons
x✝ x : Nat
xs : List Nat
tail_ih✝ : insert x✝ xs ≠ []
⊢ insert x✝ (x :: xs) ≠ []
simp [insert]
no goals
case cons
x✝ x : Nat
xs : List Nat
tail_ih✝ : insert x✝ xs ≠ []
⊢ ¬(if x✝ < x then x✝ :: x :: xs else x :: insert x✝ xs) = []
split <;> simp