proposition: Lemma big_bool R (idx : R) (op : Monoid.com_law idx) (F : bool -> R): \big[op/idx]_(i : bool) F i = op (F true) (F false).
proof: Proof. by rewrite /index_enum !unlock /= Monoid.mulm1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)