proposition: Lemma count_le_length : forall P l, count P l <= length l.
proof: Proof. Proof using. gowith LibList.count_le_length. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)