proposition: Lemma filter_length_two_disjoint : forall (P Q : A-> Prop) l, (forall x, mem x l -> P x -> Q x -> False) -> length (filter P l) + length (filter Q l) <= length l.
proof: Proof. Proof using. introv. induction l; introv H. { rew_list. nat_math. } { specializes IHl. { intros. applys* H x. } repeat rewrite filter_cons. do 2 case_if; rew_list. { false* H. } { nat_math. } { nat_math. } { nat_math. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)