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