proposition: Lemma nth_decr_nth_neq sh i j : is_part sh -> is_rem_corner sh i -> i != j -> nth 0 (decr_nth sh i) j = nth 0 sh j.
proof: Proof. move=> Hpart Hcrn /negbTE Hij. rewrite -{2}(decr_nthK Hpart Hcrn). by rewrite nth_incr_nth Hij add0n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype