proposition: Lemma flatten_map_big xs f : flatten (map f xs) = \big[cat/[::]]_(x <- xs) f x.
proof: Proof. elim: xs=>/= [|x xs IH]; first by rewrite big_nil. by rewrite big_cons IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)