proposition: Lemma map_reshape T S (f : T -> S) sh s : map (map f) (reshape sh s) = reshape sh (map f s).
proof: Proof. by elim: sh s => //= sh0 sh IHsh s; rewrite map_take IHsh map_drop. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)