Somewhere that omega doesn’t work, where I’d expect it would.

why_not_omega.v

Lemma list_filterremove_less x l: (InA E.eq x l) -> length (List.filter (fun y => if E.eq_dec y x then false else true) l) < length l.
Proof.
  intros H_xinl.  induction H_xinl as [ y l' H_xy | y l' H_xl' IHH].
  Case "x = y, l = y :: l'".
    simpl.  destruct (F.eq_dec y x) as [H_yes | H_no].  
      SCase "F.eq_dec y x = yes".
      assert (length (List.filter (fun y0 : E.t => if F.eq_dec y0 x then false else true) l') <= length l') by (apply filter_length).  unfold lt.
      (* omega. *)
      apply Le.le_n_S; assumption.  (* Why doesn’t [omega] work? *)