proposition: Lemma is_part_incr_nth sh i : is_part sh -> is_add_corner sh i -> is_part (incr_nth sh i).
proof: Proof. rewrite /is_add_corner; move=> /is_partP[Hhead Hpart]. case (i =P 0) => [->{i} _ | /eqP Hi /= H]; apply/is_partP. - case: sh Hhead Hpart => [//= _ _ | s0 sh /=]; first by split=> //= [] []. move=> Hlast Hi; split; first by move: Hlast; case sh. case=> [| i]; first by apply: (leq_trans (Hi 0)) => //=. by move/(_ i.+1) : Hi. - case: i Hi H => [//= | i] _; split; first exact: last_incr_nth_non0. move: H => /= H j. case: sh Hhead Hpart H => [| s0 sh] /= Hlast Hpart Hcorn. + by exfalso; move: Hcorn; rewrite nth_nil. + rewrite !nth_incr_nth; case (i =P j) => Hi /=. * rewrite add1n; subst i. apply (leq_trans Hcorn). elim: j s0 sh {Hcorn Hlast Hpart} => //= j IHj s0 sh. case sh => [| s1 sh']; first by rewrite nth_nil. exact: IHj. * rewrite add0n. case: j Hi => //= j Hj. rewrite nth_incr_nth; case: (i =P j) => Hi. case: sh Hpart {Hlast Hcorn} => //= s1 sh Hpart. exact: (leq_trans (Hpart j.+1)). rewrite add0n. by case: sh Hpart {Hlast Hcorn}. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype