proposition: Lemma bigA_distr (R : Type) (zero one : R) (times : Monoid.mul_law zero) (plus : Monoid.add_law zero times) (I : finType) (F1 F2 : I -> R) : \big[times/one]_(i in I) plus (F1 i) (F2 i) = \big[plus/zero]_(0 <= k < #|I|.+1) \big[plus/zero]_(J in {set I} | #|J| == k) \big[times/one]_(j in I) (if j \notin J then F1 j else F2 j).
proof: Proof. pose F12 i (j : bool) := if ~~ j then F1 i else F2 i. under eq_bigr=> i. rewrite (_: plus (F1 i) (F2 i) = \big[plus/zero]_j F12 i j); last first. rewrite (bigID (fun i => i == false)) big_pred1_eq (big_pred1 true) //. by case. over. rewrite bigA_distr_bigA big_mkord (partition_big (fun i : {ffun I -> bool} => inord #|[set x | i x]|) (fun j : [finType of 'I_#|I|.+1] => true)) //=. { eapply eq_big =>// i _. rewrite (reindex (fun s : {set I} => [ffun x => x \in s])); last first. { apply: onW_bij. exists (fun f : {ffun I -> bool} => [set x | f x]). by move=> s; apply/setP => v; rewrite inE ffunE. by move=> f; apply/ffunP => v; rewrite ffunE inE. } eapply eq_big. { move=> s; apply/eqP/eqP. move<-; rewrite -[#|s|](@inordK #|I|) ?ltnS ?max_card //. by congr inord; apply: eq_card => v; rewrite inE ffunE. move=> Hi; rewrite -[RHS]inord_val -{}Hi. by congr inord; apply: eq_card => v; rewrite inE ffunE. } by move=> j Hj; apply: eq_bigr => k Hk; rewrite /F12 ffunE. } Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext