proposition: Lemma flattenK ss : reshape (shape ss) (flatten ss) = ss.
proof: Proof. by elim: ss => //= s ss IHss; rewrite take_size_cat ?drop_size_cat ?IHss. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)