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