proposition: Lemma psumn_eq k (F1 F2 : nat -> nat): (forall j, j <= k -> \sum_(i < k | i < j) F1 i = \sum_(i < k | i < j) F2 i) -> forall j, j < k -> F1 j = F2 j.
proof: Proof. pose rw := (big_ord_narrow, big_ord_recr). move=> h j; elim: j {-2}j (leqnn j)=> [|j ih] l. rewrite leqn0=> /eqP-> lt; have := h 1 lt. by rewrite !rw !big_ord0 /= !add0n=> ->. rewrite leq_eqVlt ltnS => /predU1P[->|]; last by apply/ih. move: {-2}j.+1 (leqnn j.+1)=> x le_xSj lt; have := h _ lt. rewrite !rw /=; set S1 := bigop _ _ _; set S2 := bigop _ _ _. suff <-: S1 = S2 by move/addnI. apply/eq_bigr=> /=. case=> /= i lt_ix _; apply/ih; last by apply/(ltn_trans lt_ix). by rewrite -ltnS; apply/(leq_trans lt_ix). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)