proposition: Lemma big_bool (f : bool -> R) : \big[M/idx]_(i in {:bool}) f i = M (f false) (f true).
proof: Proof. set h : 'I_2 -> bool := [eta (fun=>false) with ord0 |-> false, lift ord0 ord0 |-> true]. set h' : bool -> 'I_2 := fun x => match x with false => ord0 | true => lift ord0 ord0 end. rewrite (reindex_onto h h') /=; last by move=> i _; rewrite /h /h'; case: ifP. rewrite (eq_bigl xpredT); last first. move=> i; move: (ord2 i) => /orP[|] /eqP -> /=; first by rewrite eqxx. exact/eqP/val_inj. by rewrite big_ord_recl /= big_ord_recl big_ord0 Monoid.addm0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext