proposition: Lemma in_shape_size sh r c : in_shape sh (r, c) -> r < size sh.
proof: Proof. rewrite /in_shape; apply contraLR; rewrite -!leqNgt => Hr. by rewrite (nth_default _ Hr). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype