proposition: Lemma big_AC_mk_monoid [I : Type] r P (F : I -> T) : \big[op/x]_(i <- r | P i) F i = odflt x (oop (\big[oop/None]_(i <- r | P i) Some (F i)) (Some x)).
proof: Proof. by apply: Some_inj; rewrite some_big_AC_mk_monoid. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)