proposition: Lemma prod_hook_length_quot_row p Alpha Beta : is_part p -> corner_box p (Alpha, Beta) -> \prod_(i <- enum_box_in (decr_nth p Alpha) | i.1 == Alpha) ( (hook_length p i)%:Q / (hook_length (decr_nth p Alpha) i)%:Q ) = \prod_(0 <= j < Beta) (1 + ((hook_length p (Alpha, j))%:Q - 1)^-1).
proof: Proof. move=> Hpart Hcorn. have:= Hcorn => /andP/=[Hcrn/eqP HBeta]. have:= decr_nthK Hpart Hcrn; set p' := decr_nth p Alpha => Hp. set F := (F in _ = \prod_(i <- _) F i). rewrite big_seq_cond (eq_bigr (fun i => F i.2)) -?big_seq_cond; first last. move=> [r c] /= /andP[]; rewrite mem_enum_box_in unfold_in /= => Hin /eqP Hr. subst r. rewrite {}/F -Hp hook_length_pred hook_length_incr_nth_row /=; first last. - exact: Hin. - rewrite /p'. exact: add_corner_decr_nth. - exact: is_part_decr_nth. have: (hook_length p' (Alpha, c))%:Q != 0 by rewrite intr_eq0. move: (hook_length p' (Alpha, c)) => h Hn. rewrite -addn1; rewrite PoszD intrD. by rewrite -{4}(divff Hn) -{3}div1r -mulrDl. transitivity (\prod_(i <- [seq i.2 | i <- enum_box_in p' & i.1 == Alpha]) F i). by rewrite big_map big_filter; apply: eq_bigr. rewrite big_map /enum_box_skew filter_flatten big_flatten /= -map_comp big_map. case: (ltnP Alpha (size p')) => Halpha. - rewrite (bigD1_seq Alpha) /=; first last. + exact: iota_uniq. + rewrite mem_iota add0n. by rewrite Halpha. rewrite big_filter big_map /=. under eq_bigl do rewrite /= eq_refl. rewrite nth_nil subn0. rewrite /p' nth_decr_nth -HBeta (eq_bigr F) //. rewrite /index_iota subn0 mulrC. rewrite big1 ?mul1r // => i /negbTE Hi. by rewrite big_filter big_map big_pred0. - move: HBeta; rewrite -nth_decr_nth (nth_default _ Halpha) => ->. rewrite /index_iota /= big_nil. rewrite big_seq_cond. apply big1 => i; rewrite andbT mem_iota /= add0n => Hi. rewrite big_filter big_map big_pred0 // => j /=. exact: ltn_eqF (leq_trans Hi Halpha). Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure