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. intros. unfolds length. forwards~: LibList.filter_length_two_disjoint. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)