proposition: Lemma is_add_corner_conj_part sh r : is_part sh -> is_add_corner sh r -> is_add_corner (conj_part sh) (nth 0 sh r).
proof: Proof. case/altP: (r =P 0) => Hr; rewrite /is_add_corner /= => Hpart /orP[]. - move/eqP->. case: sh Hpart (part_head_non0 Hpart) => //= s0 sh /andP[Hs0 Hpart] Hs0n0. apply/orP; right. rewrite !nth_incr_first_n ltnn. have -> : s0.-1 < s0 by move: Hs0n0; case s0. rewrite ltnS {Hs0}. case: s0 Hs0n0 => //= s0 _. by move/is_part_conj/is_partP: Hpart => [_]; apply. - by rewrite Hr ltnn. - by rewrite (negbTE Hr). - move=> Hnthr. case: eqP => //= /eqP H. have : nth 0 sh r <= nth 0 sh r < nth 0 sh r.-1 by rewrite leqnn Hnthr. rewrite -(nth_conjE _ Hpart Hr) => /eqP. rewrite -(conj_ltnE Hpart) => ->. by move: H; case: (nth 0 sh r). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype