proposition: Lemma bigD1_ord n j (P : pred 'I_n) F : P j -> \big[op/x]_(i < n | P i) F i = op (F j) (\big[op/x]_(i < n.-1 | P (lift j i)) F (lift j i)).
proof: Proof. move=> Pj; rewrite (bigD1 j Pj) (reindex_omap (lift j) (unlift j))/=. by under eq_bigl do rewrite liftK eq_sym eqxx neq_lift ?andbT. by move=> i; case: unliftP => [k ->|->]; rewrite ?eqxx ?andbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)