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