proposition: Lemma in_shape_tab_size t i j : in_shape (shape t) (i, j) -> i < size t.
proof: Proof. by rewrite -(size_map size) -/shape; exact: in_shape_size. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted