proposition: Lemma big_pred1 (I : finType) i (P : pred I) F : P =1 pred1 i -> \big[*%M/1]_(j | P j) F j = F i.
proof: Proof. by move/(eq_bigl _ _)->; apply: big_pred1_eq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)