proposition: Lemma subseq_flatten (f' : A -> seq B) l : (forall x, x \in l -> subseq (f x) (f' x)) -> subseq (flatten (map f l)) (flatten (map f' l)).
proof: Proof. elim: l => [|a l IH] //= Hl. rewrite cat_subseq //. by apply Hl; rewrite in_cons eqxx. by apply IH => x Hx; apply Hl; rewrite in_cons Hx orbT. Qed.
imports: mathcomp(all_ssreflect fingroup perm)