proposition: Lemma SimpleCalculation : \sum_(X <- enum_trace Alpha Beta) RHSL3_trace X = (hook_length_prod p)%:Q / (hook_length_prod p')%:Q.
proof: Proof. Proof using Hpartc'. rewrite /enum_trace /trace_seq /RHSL3_trace /RHSL3 big_allpairs /=. rewrite Formula1 !expand_prod_add1_seq /index_iota ?iota_uniq //. rewrite /index_iota subn0 big_map big_distrl big_enum; apply eq_bigr=> A _. rewrite /index_iota subn0 big_map big_distrr big_enum; apply eq_bigr=> B _. rewrite /= !belast_behead_rcons !last_behead_rcons. by congr (_ * _); apply eq_big_seq => L _; rewrite mul1r. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure