law length_filter_le_sym

bend-mathlib@0.8.1.0 · list.bend:2541

import Base

2541# Filtering never makes a list longer, reversed to rewrite toward the simple side.
2542law length_filter_le_sym:
2543  for ~A: Data
2544  for ~f: A -> Bool
2545  for xs: List<&2, A>
2546  {True{} == Nat.is_le(List.length(&2, A, List.filter(~A, ~f, xs)), List.length(&2, A, xs)) : Bool}