proposition: Lemma rem_corner_conj_part sh i : is_part sh -> is_rem_corner sh i -> is_rem_corner (conj_part sh) (nth 0 sh i).-1.
proof: Proof. elim: sh i => [| s0 sh IHsh] i /=. by rewrite /is_rem_corner nth_default // nth_default //. move=> /andP[H0 Hpart]. case: i => [| i] /= H. case: s0 H0 H => // s0 _ H. apply rem_corner_incr_first_n. exact: is_part_conj. apply rem_corner_incr_first_nE; first exact: is_part_conj. exact: (IHsh _ Hpart). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype