proposition: Lemma big_pred1 (I : finType) i (P : pred I) (F : I -> X) : P =1 pred1 i -> \big[*%M/1]_(j | P j) F j ≡ F i.
proof: Proof. move/(eq_bigl _ _)->; apply: big_pred1_eq. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect)