proposition: Lemma sumn_decr_nth sh i : is_part sh -> is_rem_corner sh i -> (sumn (decr_nth sh i)) = (sumn sh).-1.
proof: Proof. move=> Hpart Hcorn. rewrite -{2}[sh](decr_nthK Hpart Hcorn). by rewrite sumn_incr_nth /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype