proposition: Lemma big_mkcond : forall I r (P : pred I) F, \big[*%M/1]_(i <- r | P i) F i === \big[*%M/1]_(i <- r) (if P i then F i else 1).
proof: Proof. move=> I r P F. elim: r => //=; try reflexivity; move=> i r HR. case P. by rewrite -> HR;reflexivity. by rewrite -> op_left_id; exact HR. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops