proposition: Lemma big_pred1_eq_id (I : finType) (i : I) F : \big[op/x]_(j | j == i) F j = op (F i) x.
proof: Proof. have [e1 <- _ [e_enum _]] := big_enumP (pred1 i). by rewrite (perm_small_eq _ e_enum) enum1 ?big_seq1_id. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)