proposition: Lemma all_sums_p2 f: nat_ord_seq f -> (allf f (fun z => z = \0o)) -> (n_all_sums f) = singleton \0o.
proof: Proof. move => ha hb; apply: set1_pr1. apply: funI_setne; exists (identity Nat); apply:permutation_id. move => y /funI_P [t tp ->]. move: (f_perm_t_ax ha tp); set g := (f_perm_t f t) => axg. move:Nat_order_wor => [wor sr]. have ses: sub emptyset (substrate Nat_order) by move => x /in_set0. have allz i:inc i (substrate Nat_order -s emptyset) -> Vg g i = \0o. move/permutationsP: tp => [[[ft injt][_ stjt]] st tt]. rewrite sr - st => /setC_P []; rewrite st /g /f_perm_t => iN _; rewrite LgV//. move: iN; rewrite - st => /(Vf_target ft); rewrite tt - (proj32 ha). apply/hb. move: (isum_p9 wor ses (nsum_p0 axg) allz); rewrite (isum_p2 _ wor). by rewrite sr -/(n_partial_sum _ _) - (nsum_p1 axg). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)