proposition: Lemma box_in_incr_nth sh i : perm_eq ((i, nth 0 sh i) :: enum_box_in sh) (enum_box_in (incr_nth sh i)).
proof: Proof. apply uniq_perm. - rewrite /= enum_box_skew_uniq andbT mem_enum_box_skew unfold_in. by rewrite /= nth_nil leq0n ltnn. - exact: enum_box_skew_uniq. - move=> [r c]; rewrite !inE !mem_enum_box_skew !unfold_in /in_shape nth_nil /=. apply/idP/idP => [/orP[/eqP[-> ->]|] | ]. * by rewrite nth_incr_nth eq_refl add1n ltnS. * move => /leq_trans; apply. by rewrite nth_incr_nth; exact: leq_addl. + rewrite nth_incr_nth xpair_eqE eq_sym. case: eqP => [-> {r} | Hri] /=; last by rewrite add0n. by rewrite add1n ltnS leq_eqVlt. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype