proposition: Lemma nds_type0 n X: natp n -> \2c <=c n -> nds_ax X n -> (exists2 i, i<c n & X i = \0o) -> exists2 Y, nds_ax Y n & nds_card X n <c nds_card Y n.
proof: Proof. move => nN ln2 ax Hx. have nz:= (card_ge2_nz ln2). move: (cpred_pr nN nz); set m := cpred n; move => [mN nv]. have: exists Z, [/\ nds_ax Z n, nds_card X n = nds_card Z n & Z m = \0o]. move: Hx => [i lin Xz]. have iin: inc i n by apply /(NltP nN). move /(NltP nN): (cpred_lt nN nz) => ipn. move:(transposition_prop nN iin ipn). set G := Lf _ _ _; move => [Gp Gi Gpn Go GGx]. move:(proj1(nds_ax_perm nN ax Gp));set Z := (fun z => X (Vf G z)) => axZ. by exists Z; rewrite (nds_card_perm_inv nN ax Gp) /m /Z Gpn. move => [Z [axZ -> Z0]]; clear X ax Hx. wlog xnz: Z Z0 axZ/ exists2 i, i <c m & Z i <> \0o. move=> Ha; case: (p_or_not_p(exists2 i, i <c m & Z i <> \0o)) => Hx. by apply: Ha. have Xn: forall i, i <c n -> natp (Z i). rewrite nv => i /(cltSleP mN)/ cle_eqVlt; case. move ->;rewrite Z0; apply:NS0. move => im; case: (equal_or_not (Z i) \0o) => h; first by rewrite h; fprops. by case: Hx; exists i. pose X1 := fun i => Yo (i = m) \0o \1o. have X1n: forall i, i <c n -> natp (X1 i). rewrite /X1; move => i ii; Ytac h; fprops. have X1m: X1 m = \0o by rewrite /X1; Ytac0. move: ln2; rewrite - succ_one {1}nv;move/(cleSSP CS1 (CS_nat mN))/cge1P => n1. have X10: exists2 i, i <c m & X1 i <> \0o. exists \0c => //; rewrite /X1 (Y_false (proj2 n1)); fprops. have ax1: nds_ax X1 n by move => i /X1n /OS_nat. by rewrite (nds_of_nat nN Xn) -(nds_of_nat nN X1n); apply: Ha. have lmn: m <c n by move: (cltS mN); rewrite nv. have axm: nds_ax Z m by move => i lin; apply: axZ; move: (clt_ltT lin lmn). have alsp: forall v, inc v (nds_sums Z m) -> \0o <o v. move => v /funI_P [s sp ->]. move: (nds_ax_perm mN axm sp) => [ha hb]. apply:(osum_fnz mN ha). move/permutationsP: sp => bsp. move: (inverse_bij_bp bsp) => [[[isb _] _] iss ist]. move: bsp=> [bs ss ts]. move: xnz => [k lkm Zk]. have ktf: inc k (target s) by rewrite ts; apply/(NltP mN). move: (inverse_V bs ktf); rewrite -/k => kv. exists (Vf (inverse_fun s) k); last by rewrite kv. by apply/(NltP mN); Wtac; rewrite iss - ts. have [e oe ep]: exists2 e, ordinalp e & (forall i, i<c m -> Z i <o oopow e). suff: exists2 x, ordinalp x & (forall i, i<c m -> Z i <=o x). move => [x ox xle]; move:(OS_succ ox) => osx; exists (osucc x) => //. move => i /xle le; apply: (ole_ltT le); apply/oleSltP. by apply:ord_eps_p1. clear nv Z0 xnz lmn alsp. move: m mN axm; apply:Nat_induction. move => _; exists \0o; [ exact: OS0 | by move => i /clt0]. move => m mN Hrec h. move: (true_below_rec mN h)=> [sa sb]. move: (Hrec sa) => [a oa ap]. move:(omax_p1 oa sb) => [sc sd]. exists (omax a (Z m)); first exact: (proj32 sc). move => i /(cltSleP mN) /cle_eqVlt; case; first by move ->. move/ap => le1; apply: (oleT le1 sc). pose T u i := Yo (i = m) u (Z i). have To u: ordinalp u -> nds_ax (T u) n. rewrite nv /T => ou i /(cltSleP mN) /cle_eqVlt [] li; try Ytac0 => //. by rewrite (Y_false (proj2 li)); apply: axm. have Tuv u: ordinalp u -> forall v, inc v (nds_sums Z m) -> inc (u +o v) (nds_sums (T u) n). move => ou v /funI_P [s sp ->]. move: (extension_perm mN sp). set es := extension s m m; move => [esp esout esin]. rewrite - nv in esp; apply/funI_P; ex_tac. rewrite/nds_sc nv (osum_fS _ mN) esout/T; Ytac0; congr osum2. apply: (osumf_exten mN) => i /(NltP mN) lin; rewrite esin //. have: inc (Vf s i) m by move/permutationsP: sp => [[[ff _] _ ] sf tf]; Wtac. by move/(NltP mN) => /proj2 nn; Ytac0. set u := oopow e. have ou:= (OS_oopow oe). have us: inc u (nds_sums (T u) n). apply/funI_P; move: (rotation_prop mN); rewrite - nv. set f := Lf _ _ _; set g := Lf _ _ _. move => [pf pg ifg [fo fa1 fa2 gn ga]]. exists f; first exact. rewrite /T /nds_sc nv (osum_negl_rec oe) //. by rewrite fo; Ytac0. by move => i lin; rewrite (fa1 _ lin) (Y_false (proj2 lin)); apply: ep. move: (To u ou) => axT. exists (T u); first exact: (To u ou). apply/(cleSltP (NS_nds_card Z nN)). have ->: nds_card Z n = cardinal(nds_sums Z m). rewrite /nds_card /nds_sums; congr cardinal. set_extens z; last first. rewrite nv; move: (Tuv _ OS0) => rb zv. have oz: ordinalp z. move/funI_P: zv =>[w wp ->]; exact: (proj2(nds_ax_perm mN axm wp)). move: (rb _ zv); rewrite (osum0l oz) - nv. congr inc; apply:(nds_sums_exten nN)=> i lin; rewrite /T. by Ytac h => //; rewrite h Z0. move => /funI_P [f fp ->]. rewrite nv in fp; move: (partial_rotation mN fp). set k := Vf (inverse_fun f) m. set (g:= fun i => Yo (i <c k) (Vf f i) (Vf f (csucc i))). move => [lekn fk axg gp]. apply/funI_P; ex_tac. move: (cdiff_pr lekn) (NS_diff k mN); set q:= _ -c _ => sb qN. move/(cleSSP (proj31 lekn) (proj32 lekn)): (lekn) => li0n1. have kN:=(NS_le_nat lekn mN). have skN:=(NS_succ kN). pose g0 i := Z (Vf (Lf g m m) i). pose f0 i := Z (Vf f i). move/permutationsP: (fp) => [bf sf tf]; move: (proj1(proj1 bf)) => ff. rewrite -nv in sf tf. have ax1: nds_ax f0 (csucc k +c q). rewrite (csum_Sn _ kN) sb - nv => i lin; rewrite /f0; apply: axZ. by apply/(NltP nN); Wtac; rewrite sf; apply/(NltP nN). have ax2: (nds_ax g0 (k +c q)). rewrite sb => i/(NltP mN) lin; rewrite /g0 LfV//; apply axm. by move: (axg _ lin) => /(NltP mN) h1. have osa: ordinalp (osumf f0 k). apply: (OS_osumf kN) => i lin; rewrite /f0; apply: axZ. apply/(NltP nN); Wtac; rewrite sf;apply/(NltP nN). exact: (clt_ltT lin (cle_ltT lekn lmn)). move:(osum_fA skN qN ax1);rewrite (csum_Sn _ kN) sb nv -/(nds_sc _ _ _) => ->. rewrite (osum_fS _ kN) {2} /f0 fk Z0 (osum0l osa). rewrite /nds_sc - {3} sb (osum_fA kN qN ax2); apply: f_equal2. apply:(osumf_exten qN) => i lim; rewrite /f0/g0 /g. have ha: inc (i +c k) m. apply /(NltP mN); rewrite -{1} sb (csumC _ q); apply:(csum_Mlteq kN lim). have hb: ~(i +c k <c k). move:(csum_Mle0 i (proj31 lekn)) => ua ub; case: (cleNgt ua ub). by rewrite LfV//; Ytac0; rewrite (csum_nS _ kN). apply:(osumf_exten kN) => i lim; rewrite /f0/g0 /g. rewrite LfV //; [ by Ytac0 |apply /(NltP mN); apply: (clt_leT lim lekn) ]. have alsp': ~inc \0o (nds_sums Z m) by move /alsp; case. rewrite - (csucc_pr alsp'). have: injection (Lf (osum2 u) (nds_sums Z m +s1 \0o) (nds_sums (T u) n)). have H x: inc x (nds_sums Z m +s1 \0o) -> ordinalp x. case /setU1_P; last by move ->; apply: OS0. move => /funI_P [p pp ->]; exact:proj2 (nds_ax_perm mN axm pp). apply: lf_injective. by move => x/setU1_P; case; [ apply: Tuv | move ->; rewrite (osum0r ou)]. move => x y /H xs /H ys; apply: (osum2_simpl xs ys ou). by move /inj_source_smaller; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)