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