proposition: Lemma rev_reshape sh s : size s = sumn sh -> rev (reshape sh s) = map rev (reshape (rev sh) (rev s)).
proof: Proof. move=> sz_s; apply/(canLR revK)/eq_from_flatten_shape. rewrite reshapeKr ?sz_s // -rev_flatten reshapeKr ?revK //. by rewrite size_rev sumn_rev sz_s. transitivity (rev (shape (reshape (rev sh) (rev s)))). by rewrite !reshapeKl ?revK ?size_rev ?sz_s ?sumn_rev. rewrite shape_rev; congr (rev _); rewrite -[RHS]map_comp. by under eq_map do rewrite /= size_rev. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)