proposition: Lemma reshape_rcons s sh n (m := sumn sh) : m + n = size s -> reshape (rcons sh n) s = rcons (reshape sh (take m s)) (drop m s).
proof: Proof. move=> Dmn; apply/(can_inj revK); rewrite rev_reshape ?rev_rcons ?sumn_rcons //. rewrite /= take_rev drop_rev -Dmn addnK revK -rev_reshape //. by rewrite size_takel // -Dmn leq_addr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)