proposition: Lemma big_pred1 : forall (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=> I i P F eqP; rewrite -> (eq_bigl _ _ eqP); exact: big_pred1_eq. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops