proposition: Lemma length_filter A f (l : list A) : length (filter f l) <= length l.
proof: Proof. induction l; ins; desf; ins; lia. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation