proposition: Lemma big1_seq : forall (I : eqType) r (P : pred I) F, (forall i, P i && (i \in r) -> F i === 1) -> \big[*%M/1]_(i <- r | P i) F i === 1.
proof: Proof. move=> I r P F eqF1; rewrite -> big_cond_seq; rewrite -> (eq_bigr _ eqF1). by rewrite -> big1_eq;reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops