proposition: Lemma tabsh_to_wordK t : rev (reshape (rev sh) (to_word (val t))) = t.
proof: Proof. Proof using. by rewrite /= -(shape_tabsh t); apply: to_wordK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted