rw [Nat.add_comm _ 1, Nat.add_assoc]
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length xs + (length as + 1) ≤ length xs + 1 + length as
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length xs + (1 + length as) ≤ length xs + (1 + length as)