proposition: Lemma is_rem_cornerP sh i : is_part sh -> (i < size sh) && (~~ in_shape sh (i.+1, (nth 0 sh i).-1)) = (is_rem_corner sh i).
proof: Proof. rewrite /is_rem_corner /in_shape -ltnNge => Hpart. apply/idP/idP. - move=> /andP[/(nth_part_non0 Hpart)]. by case: (nth 0 sh i). - case: (ltnP i (size sh)) => Hi; last by rewrite [nth 0 sh i]nth_default. have:= nth_part_non0 Hpart Hi. by case: (nth 0 sh i) => pi //= _ ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype