proposition: Theorem nsum_p13b f: nat_ord_seq f -> finite_set (n_all_sums f).
proof: Proof. move => axf. move:(nsum_p10g axf). set E := (n_sum_small_idx f); set rho := n_sum_rem f => sv. have fse: finite_set E by apply: nsum_p10c. have sEN: sub E Nat. by rewrite /E/n_sum_small_idx; Ytac h; apply: Zo_S. move: (proj1 (sub_nat_isomorphism sEN) fse) =>[n nN [g1 is1]]. move: (nsum_p0 axf) => ax. move:Nat_order_wor => [wor sr]. have ses: sub E (substrate Nat_order) by ue. move: (induced_wor wor ses) (iorder_sr (proj1 wor) ses). set rE := (induced_order Nat_order E) => worE srE. set fE := restr f E. have eq1: n_partial_sum f E = ipartial_sum fE rE (substrate rE). rewrite /n_partial_sum /ipartial_sum /rE srE (iorder_trans _ (@sub_refl E)). by rewrite /fE double_restr. have axE: [/\ fgraph fE, domain fE = substrate rE & allf fE ordinalp]. rewrite /fE Lgd; split; fprops; hnf; aw => t tE; rewrite LgV//. by apply:(proj33 axf); rewrite (proj32 axf); apply: sEN. have sns: sub n (substrate Nat_order). rewrite sr => t tN; apply: (NS_inc_nat nN tN). move: (induced_wor wor sns) (iorder_sr (proj1 wor) sns). set rn := (induced_order Nat_order n) => worb srn. move: (isum_p11 worE is1 axE); rewrite - eq1 -/rE -/rn srn. set b := Lg _ _; move => eq2. pose bpt t := Lg n (fun i => Vg b (Vf t i)). set F1 := fun_image (permutations n) (fun t => ipartial_sum (bpt t) rn n). set F2 := fun_image F1 (fun x => x +o rho). suff h: sub (n_all_sums f) F2. have fs: finite_set F2. apply: finite_fun_image; apply: finite_fun_image. apply/card_finite_setP; rewrite (card_permutations (finite_set_nat nN)). by rewrite (card_card (CS_nat nN)); apply: NS_factorial. exact: (sub_finite_set h fs). move => v /funI_P [t pt ->]. rewrite (proj33 (nsum_p12c axf pt)); apply: funI_i. move/permutationsP:pt => tprop. rewrite -/E; set F := fun_image _ _. have cF: F =c E. apply: cardinal_fun_image => x y xs ye. move: (inverse_bij_bp tprop) =>[ [[_ hh] _] st _]. by apply: hh; rewrite st; apply: sEN. move:tprop =>[bt st tt]. have sFN: sub F Nat. move => x /funI_P [y yR ->]; rewrite - st. have yt: inc y (target t) by rewrite tt; apply: sEN. exact: (inverse_Vis bt yt). have sfs: sub F (substrate Nat_order) by ue. move: (induced_wor wor sfs) (iorder_sr (proj1 wor) sfs). set rF := (induced_order Nat_order F) => worF srF. set fF := restr (f_perm_t f t) F. have ->: n_partial_sum (f_perm_t f t) F = ipartial_sum fF rF (substrate rF). rewrite /n_partial_sum /ipartial_sum /rF srF (iorder_trans _ (@sub_refl F)). by rewrite /fE double_restr. have axF: [/\ fgraph fF, domain fF = substrate rF & allf fF ordinalp]. rewrite /fF; aw; split; fprops; hnf; aw => x tF; rewrite LgV//. have xN: natp x by apply: sFN. rewrite /f_perm_t LgV//; apply:(proj33 axf); rewrite (proj32 axf). Wtac; [ fct_tac | ue ]. have fsf: finite_set F. by apply/card_finite_setP; rewrite cF; apply/card_finite_setP. move: (proj1 (sub_nat_isomorphism sFN) fsf) =>[n1 n1N [g2 is2]]. have eq4: n1 = n. move: is1 is2 => [_ _ [ba sa ta] _] [_ _ [bb sb tb] _]. move: (card_bijection ba)(card_bijection bb). have sms: sub n1 (substrate Nat_order). rewrite sr => x xN; apply: (NS_inc_nat n1N xN). move: (iorder_sr (proj1 wor) sms) => srm. rewrite sa ta sb tb srE srF srn srm cF (card_card (CS_nat nN)). by rewrite (card_card (CS_nat n1N)); move => <- <-. rewrite eq4 in is2. rewrite (isum_p11 worF is2 axF) srn -/rn. pose cv i := Vf g1 (Vf t (Vf (inverse_fun g2) i)). move: is1 is2 => [_ _ [bg1 sg1 tg1] _] [_ _ [bg2 sg2 tg2] _]. move: (proj1 (proj1 bg1))(proj1 (proj1 bg2)) => fg1 fg2. move: sg1 tg1 sg2 tg2. rewrite srE srF srn => sg1 tg1 sg2 tg2. have ha i: inc i n -> inc (Vf (inverse_fun g2) i) F. by rewrite -tg2 - sg2 => it ;apply: (inverse_Vis bg2). have hb i: inc i n -> inc (Vf t (Vf (inverse_fun g2) i)) E. move/ha => /funI_P [x xÊ ->]; rewrite (inverse_V bt) => //. by rewrite tt; apply: sEN. have hc: lf_axiom cv n n by move => i /hb vE; rewrite/cv; Wtac. set c := Lf cv n n. have fpc:function_prop c n n. by rewrite /c/function_prop; saw; apply: lf_function. have cp: inc c (permutations n). apply: (permutation_if_inj (finite_set_nat nN) fpc). apply: lf_injective => // x y xn yn; rewrite /cv. move: (hb _ xn) (hb _ yn); rewrite - sg1 => xa ya. move: (sFN _ (ha _ xn)) (sFN _ (ha _ yn)); rewrite - st => xb yb. move/ (proj2 (proj1 bg1) _ _ xa ya). move/ (proj2 (proj1 bt) _ _ xb yb)=> eqxx. rewrite - tg2 in xn yn. by rewrite - (inverse_V bg2 xn) - (inverse_V bg2 yn) eqxx. apply/funI_P; ex_tac; congr (ipartial_sum _ rn n). apply: Lg_exten => i iE. have ra: inc (Vf (inverse_fun g2) i) F by apply: ha. have rb: inc (Vf (inverse_fun g2) i) Nat by apply: sFN; apply: ra. have rc: inc (Vf c i) n by rewrite /c LfV//; apply:hc. have rd: inc (Vf (inverse_fun g1) (Vf c i)) E. by rewrite - sg1; apply: (inverse_Vis bg1); rewrite tg1; apply: rc. have re: inc (Vf t (Vf (inverse_fun g2) i)) (source g1). by rewrite sg1; apply: hb. by rewrite /fF/f_perm_t /b /fE/c/cv !LgV// LfV// (inverse_V2 bg1 re). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)