proposition: Lemma get_tab_default t rc : ~~ in_shape (shape t) rc -> get_tab t rc = inh.
proof: Proof. Proof using. rewrite /in_shape /get_tab -leqNgt nth_shape => Hc. exact: nth_default. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted