proposition: Lemma conj_hookpartn d k : k < d -> conj_intpartn (hookpartn d k) = hookpartn d (d.-1 - k).
proof: Proof. case: d => // d; rewrite ltnS; case: k => [_|k ltkd]. by rewrite hookpartn_col subn0 hookpartn_row conj_colpartn. apply val_inj; rewrite /= !hookpartnE ?ltnS ?leq_subr //. have -> : k.+2 :: nseq (d - k.+1) 1 = incr_first_n [:: k.+1] (d - k). move: ltkd; rewrite -subn_gt0 /= subnS. by case: (d - k). by rewrite conj_part_ind ?subn_gt0 // subKn //= -subSn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype