proposition: Lemma length_remove : forall l a, length (LibList.remove a l) <= length l.
proof: Proof. Proof using. intros. rewrite remove_as_filter. applys length_filter. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)