proposition: Lemma in_flat_map l y : In y (flat_map l) <-> exists x, In x l /\ In y (f x).
proof: Proof. rewrite flat_map_concat_map, in_concat. split. - intros [l' [[x [<- ?]] %in_map_iff ?]]. now exists x. - intros [x [? ?]]. exists (f x). now split; [apply in_map|]. Qed.
imports: PeanoNat