proposition: Lemma big1_eq : forall I r (P : pred I), \big[*%M/1]_(i <- r | P i) 1 === 1.
proof: Proof. move=> *; rewrite -> big_const_seq. elim: (count _ _); try reflexivity; move=> n //= Heq; rewrite -> Heq; apply op_right_id. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops