exact show x.size % 2 < 2 from Nat.mod_lt x.size (by decide)
case refine_1.refine_2.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ Nat.succ (Subarray.size x % 2) ≤ Nat.succ 1
no goals