proposition: Lemma expand_prod_add1_seq (S : seq T) : uniq S -> \prod_(i <- S) (1 + alpha i) = \sum_(s : subseqs S) \prod_(i <- s) alpha i.
proof: Proof. Proof using. elim: S => [| a S IHs] aS_uniq //. by rewrite (big_subseqs0 (fun s => \prod_(i <- s) alpha i)) !big_nil. have /= /andP[_ S_uniq] := aS_uniq. rewrite (big_subseqs_cons (fun s => \prod_(i <- s) alpha i) aS_uniq) /=. rewrite big_cons {}IHs // addrC mulrDl mul1r; congr (_ + _). rewrite mulr_sumr; apply eq_bigr => /= [[s subs] _] /=. by rewrite big_cons. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure