proposition: Lemma reshapeKr sh s : size s <= sumn sh -> flatten (reshape sh s) = s.
proof: Proof. elim: sh s => [[]|n sh IHsh] //= s sz_s; rewrite IHsh ?cat_take_drop //. by rewrite size_drop leq_subLR. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)