proposition: Lemma partdom_conj_intpartn sh1 sh2 : (sh2^# <= sh1^#)%O = (sh1 <= sh2)%O.
proof: Proof. suff {sh1 sh2} decr sh1 sh2 : (sh1 <= sh2)%O -> (sh2^# <= sh1^#)%O. by apply/idP/idP => /decr //; rewrite !conj_intpartnK. move => /partdomP Hdom; apply/partdomP => i. rewrite -!sum_conj. rewrite !sum_minn !sumn_intpartn; apply: leq_sub => //. pose c1 := nth 0 (conj_part sh1) i. have Hc1 : c1 <= size sh1 by rewrite /c1 -conj_leqE // nth_default. have -> : \sum_(l <- sh1) (l - i) = \sum_(l <- take c1 sh1) (l - i). rewrite -{1}(cat_take_drop c1 sh1) !big_cat /=. rewrite [X in _ + X]big_seq [X in _ + X]big1 ?addn0 // => /= j jin. rewrite -(nth_index 0 jin) nth_drop. apply/eqP; rewrite subn_eq0. by rewrite conj_leqE // leq_addr. rewrite -(leq_add2r (c1 * i)) -{2}(size_takel Hc1) -sum1_size. rewrite big_distrl -big_split /=. rewrite big_seq [X in X <= _](eq_bigr id) -?big_seq; first last. move=> j /(mem_takeP 0) [pos Hpos ->{j}]. rewrite mul1n; apply: subnK. apply ltnW; rewrite conj_ltnE // -/c1. exact: (leq_trans Hpos (geq_minl _ _)). move/(_ c1): Hdom; rewrite !sumnE => /leq_trans; apply. rewrite -{2}(cat_take_drop c1 sh2) !big_cat /= addnC addnA. apply: (leq_trans _ (leq_addr _ _)); rewrite -sumnE sumn_take. rewrite [X in _ <= X](_ : _ = \sum_(0 <= i0 < c1) maxn i (nth 0 sh2 i0)). by apply leq_sum => j _; apply leq_maxr. rewrite sum_take ?sub0n //. rewrite -{1}(subn0 c1) -sum_nat_const_nat. rewrite -big_split; apply eq_bigr => /= j _. by rewrite maxnE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype