proposition: Lemma mult_altern_oapp p d : is_part p -> size p <= n -> 'a_(mpart p + rho) * (symp_pol n R d.+1) = \sum_(i < n) oapp (fun ph => (-1) ^+ ph.2.-1 *: 'a_(mpart ph.1 + rho)) 0 (add_ribbon p d i).
proof: Proof. move=> partp szp; rewrite mult_altern_symp_pol. apply eq_bigr => i _ /=. case Hrib : add_ribbon => [[sh h]|] /=. by rewrite (alt_straight_add_ribbon _ partp szp Hrib). by rewrite (alt_straight_add_ribbon0 _ partp szp) // Hrib. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint perm fingroup tuple vector rat) mathcomp(ssrcomplements freeg mpoly monalg) sorted tools ordtype permuted partition skewpart antisym Schur_mpoly Schur_altdef sympoly homogsym