proposition: Theorem Frobenius_ident_rat : 1 / (n`!)%:Q = \sum_(p : 'P_n) 1 / (hook_length_prod p)%:Q ^+ 2.
proof: Proof. Proof using. rewrite -[RHS]mulr1. have Hfn0 : n`!%:Q != 0 by rewrite intr_eq0 eqz_nat -lt0n fact_gt0. rewrite -{5}(@divff _ ((n`!%:Q) ^+ 2)); last by rewrite sqrf_eq0. rewrite mulrA mulr_suml. rewrite (eq_bigr (fun p : 'P_n => ((n`! %/ (hook_length_prod p)) ^ 2)%N%:Q)); first last. move=> p _; rewrite PoszM intrM. have -> : (n`! %/ hook_length_prod p)%:Q = (n`!)%:Q / (hook_length_prod p)%:Q. rewrite -[LHS]mulr1 -{2}(@divff _ (hook_length_prod p)%:Q); first last. by rewrite intr_eq0 eqz_nat /=; apply: (hook_length_prod_non0 p). rewrite !mulrA -intrM -PoszM. have:= hook_length_prod_div p. by rewrite sumn_intpartn dvdn_eq => /eqP ->. by rewrite -expr2 expr_div_n mulrC mul1r. rewrite -!(big_morph intr (@intrD _) (id2 := 0)) //=. rewrite -!(big_morph Posz PoszD (id2 := 0%N)) //=. rewrite -Frobenius_ident expr2. by rewrite invfM mulrA divff. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype choice ssrnat seq ssrint div rat fintype finset bigop path ssralg ssrnum order) ordtype partition tableau Schensted std stdtab hook