proposition: Lemma filter_last : forall x l P, filter P (l & x) = filter P l ++ (If P x then x::nil else nil).
proof: Proof. Proof using. intros. rewrite~ filter_app. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)