proposition: Lemma Zlength_filter {A} (f : A -> bool) l : (Zlength (filter f l) = Zlength l - Zlength (filter (no f) l))%Z.
proof: Proof. repeat rewrite Zlength_correct. rewrite <-(length_filter f l). zify. lia. Qed.
imports: Arith ZArith List Lia