proposition: Lemma add_corner_decr_nth sh i : is_part sh -> is_rem_corner sh i -> is_add_corner (decr_nth sh i) i.
proof: Proof. move=> Hpart Hout; rewrite /is_add_corner /=. case: i Hout => [// | i] Hout; rewrite [i.+1.-1]/=. apply/orP; right. rewrite nth_decr_nth nth_decr_nth_neq //; last by rewrite eq_sym ltn_eqF. move: Hout; rewrite /is_rem_corner => Hi2. move/is_partP : Hpart => [_ Hdecr]. apply: leq_trans _ (Hdecr i). by move: Hi2; case: (nth 0 sh i.+1). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype