proposition: Lemma to_wordK t : rev (reshape (rev (shape t)) (to_word t)) = t.
proof: Proof. Proof using. by rewrite -shape_rev /to_word flattenK revK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted