proposition: Lemma conj_part_incr_nth sh i : is_part sh -> is_add_corner sh i -> conj_part (incr_nth sh i) = incr_nth (conj_part sh) (nth 0 sh i).
proof: Proof. elim: sh i => [| s0 sh IHsh] i /=. by rewrite /is_add_corner /= !nth_nil => _ /orP[] // /eqP ->. move=> /= /andP[H0 Hpart]. case: i => [_ | i Hcrn]/=. have Hszconj: (size (conj_part sh) <= s0)%N. rewrite (size_conj_part Hpart). move: H0; case sh => [| n _] //=; exact: ltnW. have Hszn : size (incr_first_n (conj_part sh) s0.+1) = s0.+1. by rewrite size_incr_first_n; last exact: (leq_trans Hszconj). apply (eq_from_nth (x0 := 0)). - rewrite Hszn. by rewrite size_incr_nth ltnNge (size_incr_first_n Hszconj) leqnn /=. - move=> i; rewrite Hszn => Hi. rewrite nth_incr_nth !nth_incr_first_n Hi ltn_neqAle. move: Hi; rewrite ltnS eq_sym => ->. by case: eqP => /= _; rewrite ?add0n ?add1n. rewrite (IHsh _ Hpart); first exact: incr_first_n_nthC. by move: Hcrn => /=; case: i. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype