proposition: Lemma mem_enum_box_skew : enum_box_skew =i in_skew inner outer.
proof: Proof. move=> [r c]; apply/allpairsPdep/idP. move=> [r'][c'][_] /[swap] [[<-{r'} <-{c'}]]. rewrite mem_iota /in_skew unfold_in /=. case: (leqP (nth 0 inner r) (nth 0 outer r)) => [inout | /ltnW]. by rewrite subnKC. rewrite -subn_eq0 => /eqP ->; rewrite addn0. by move=> /andP[/leq_ltn_trans/[apply]]; rewrite ltnn. rewrite unfold_in -/(in_skew _ _ (r, c)) in_skewE => /andP[rcinn rcout]. exists r, c; rewrite !mem_iota /= !add0n (in_shape_size rcout); split => //. rewrite /in_shape /= -?leqNgt in rcinn rcout. by rewrite rcinn /= subnKC // (leq_trans rcinn (ltnW rcout)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype