proposition: Lemma in_conj_part_impl sh : is_part sh -> forall r c, in_shape sh (r, c) -> in_shape (conj_part sh) (c, r).
proof: Proof. rewrite /in_shape. elim: sh => [| s0 s IHs] Hpart r c. by rewrite /is_rem_corner nth_default // nth_default //. have:= Hpart => /= /andP[Hhead Hparts]. rewrite nth_incr_first_n. case: r => [ -> // | r] /= H. move/is_part_ijP : Hpart => [_ /(_ _ _ (leq0n r.+1))/=]. move=> /(leq_trans H) ->. by rewrite ltnS; exact: IHs. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype