∀ {α : Type u_1} [inst : DecidableEq α] {a : α} (l₁ l₂ : List α),
  (List.filter (fun x => decide (x = a)) l₁).length + 1 ≤ (List.filter (fun x => decide (x = a)) l₂).length →
    (List.filter (fun x => decide (x = a)) l₁).length < (List.findIdxs (fun x => decide (x = a)) l₂).length