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