proposition: Lemma in_part_le sh r c j k : is_part sh -> in_shape sh (r, c) -> j <= r -> k <= c -> in_shape sh (j, k).
proof: Proof. rewrite /in_shape => /is_part_ijP[_ Hpart] Hcr /Hpart Hrj Hkc. exact: leq_ltn_trans Hkc (leq_trans Hcr Hrj). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype