proposition: Lemma big_pred1_eq (I : finType) (i : I) (F : I -> X) : \big[*%M/1]_(j | j == i) F j ≡ F i.
proof: Proof. rewrite -big_filter filter_pred1_uniq //; first by rewrite big_seq1. solve [by rewrite /index_enum -?enumT ?enum_uniq |exact: index_enum_uniq]. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect)