proposition: Lemma remove_not_mem : forall x l, ~ mem x l -> remove x l = l.
proof: Proof. Proof using. intros. applys filter_eq_self_of_mem_implies_P. intros y My ->. false. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)