proposition: Lemma filter_length_partition : forall P l, length (filter (fun x => P x) l) + length (filter (fun x => ~ P x) l) = length l.
proof: Proof. Proof using. introv. induction l. { rew_list. nat_math. } { repeat rewrite filter_cons. repeat case_if; rew_list; math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)