proposition: Lemma length_filter : forall l P, length (filter P l) <= length l.
proof: Proof. Proof using. intros. unfolds length. forwards~: LibList.length_filter l P. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)