proposition: Lemma nsum_p13a f t: nat_ord_seq f -> inc t (permutations Nat) -> small_set (n_sum_small_idx f) -> n_sum f = n_sum (f_perm_t f t).
proof: Proof. move => ha hb hd. move:Nat_order_wor => [wor sr]. move:(nsum_p12c ha hb) => [_ -> ->]; apply: f_equal2=> //. rewrite /n_partial_sum. case/small_set_pr: hd. by move ->; rewrite funI_set0 /n_partial_sum !isum_p2. move => [n nE]; rewrite nE funI_set1. have nN: natp n. move: (set1_1 n); rewrite - {1} nE. by rewrite/n_sum_small_idx; Ytac h; move/Zo_S. have ns: inc n (substrate Nat_order) by ue. move: (nsum_p0 ha) => axf. move:(nsum_p0 (f_perm_t_ax ha hb)) => axg. move/permutationsP: (hb) => [bt st tt]. have xst: inc n (target t) by ue. move: (inverse_Vis bt xst); rewrite st => yN. move: (yN); rewrite - sr => ysr. rewrite /n_partial_sum (isum_p3 wor axf ns). by rewrite (isum_p3 wor axg ysr) /f_perm_t LgV// (inverse_V bt xst). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)