proposition: Lemma rev_flatten ss : rev (flatten ss) = flatten (rev (map rev ss)).
proof: Proof. by elim: ss => //= s ss IHss; rewrite rev_cons flatten_rcons -IHss rev_cat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)