proposition: Lemma length_remove_mem : forall x l, mem x l -> length (LibList.remove x l) < length l.
proof: Proof. Proof using. intros. unfolds length. forwards~: LibList.length_remove_mem. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)