proposition: Lemma in_shape_tab i j t : in_shape (shape t) (i, j) -> j < size (nth [::] t i).
proof: Proof. move=> Hin; have:= Hin; rewrite /in_shape /shape (nth_map [::]) //. exact: (in_shape_tab_size Hin). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted