proposition: Lemma del_rem_corner sh i : last 1 sh != 0 -> is_part (incr_nth sh i) -> is_rem_corner (incr_nth sh i) i = is_part sh.
proof: Proof. move=> Hn0 /is_partP[_ Hpart1]. rewrite/is_rem_corner; apply/idP/idP. - move=> Hcorn; apply/is_partP; split; first exact Hn0. move=> j; move: Hcorn (Hpart1 j). rewrite !nth_incr_nth (@ltn_eqF i i.+1) // eq_refl add0n add1n ltnS => Hcorn. case (eqP (y:=j)) => [<- // | _]. by case eqP => [Hi |_]; rewrite !add0n // add1n; apply: ltnW. - move=> /is_partP => [] [_ /(_ i)]. by rewrite !nth_incr_nth (@ltn_eqF i i.+1) // eq_refl add0n add1n ltnS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype