∀ {α : Type u_1} [inst_1 : DecidableEq α] {g : Equiv.Perm α} {a : α} (w w_1 : α)
  (h :
    List.findIdxNth (fun x => decide (x = w)) [g (g a)] (List.idxOfNth w [g (g a)] 1) + 1 ≤
      (List.filter (fun x => decide (x = w_1)) [g (g a)]).length),
  (List.findIdxs (fun x => decide (x = w_1))
        [g (g a)])[List.findIdxNth (fun x => decide (x = w)) [g (g a)] (List.idxOfNth w [g (g a)] 1)] <
    [g (g a)].length