proposition: Lemma reshapeKl sh s : size s >= sumn sh -> shape (reshape sh s) = sh.
proof: Proof. elim: sh s => [[]|n sh IHsh] //= s sz_s. rewrite size_takel; last exact: leq_trans (leq_addr _ _) sz_s. by rewrite IHsh // -(leq_add2l n) size_drop -maxnE leq_max sz_s orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)