proposition: Theorem Theorem2 : mu choose_corner (fun pair => (ends_at (Alpha, Beta) pair)%:Q) = (HLF p') / (HLF p).
proof: Proof. Proof using Hpartc'. rewrite prob_choose_corner_ends_at // -{1 2}Hp sumn_incr_nth. rewrite factS PoszM -!ratzE ratzM !ratzE. set Rhs := (RHS). have -> : Rhs = ((1 / (sumn p').+1%:Q) * (hook_length_prod p)%:Q / (hook_length_prod p')%:Q). rewrite /Rhs -!mulrA [(((hook_length_prod p')%:Q)^-1 / _)%R]mulrC !invfM !mul1r. rewrite !mulrA [X in (X / _ / _ / _)]mulrC. congr (_ * _); rewrite -!mulrA; congr (_ * _). rewrite mulrA divff; first by rewrite invrK mul1r. rewrite intr_eq0 eqz_nat -lt0n. exact: fact_gt0. rewrite {Rhs} !mul1r -[RHS]mulrA; congr (_ * _). exact: SimpleCalculation. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure