proposition: Lemma all_sum1_p1 f: nat_ord_seq f -> ordinal_set (n_all_sums f).
proof: Proof. move => ax y /funI_P [t tp ->]. by move: (f_perm_t_ax ax tp) => ay; apply: OS_nsuma. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)