proposition: Lemma card_sincreasing_Nat (r := Nat_order) : functions_sincr r r =c functions Nat Nat.
proof: Proof. rewrite - card_increasing_Nat. set fNN := functions Nat Nat. pose D f := fun i => Yo (i = \0c) (Vf f \0c) (Vf f i -c (Vf f (cpred i))). pose S f := fun i => csumb (csucc i) (Vf f). have Hu f: inc f fNN -> natp (Vf f \0c). move=> /functionsP [ff sf tf]. rewrite /natp; Wtac; rewrite sf; apply: NS0. have Ha f: inc f fNN -> (S f \0c) = Vf f \0c. move/Hu /CS_nat => cc. rewrite /S (induction_on_sum _ NS0) csum_trivial0 csum0l//. have Hb f n: natp n -> S f (csucc n) = (S f n) +c Vf f (csucc n) . by move=> nN; rewrite /S (induction_on_sum _ (NS_succ nN)). have Hc f : inc f fNN ->lf_axiom (S f) Nat Nat. move => fnn; move: (Ha _ fnn) (Hu _ fnn) => eq1 nn1. move/functionsP: fnn =>[ff sf tf]. apply: Nat_induction; first by rewrite eq1. move => n nN Hr; rewrite (Hb _ _ nN); apply: (NS_sum Hr). rewrite /natp; Wtac; rewrite sf; apply: (NS_succ nN). have Hd f: inc f fNN -> inc (Lf (S f) Nat Nat) (functions_incr r r). move => ff; apply/card_increasing_Nat_aux. have ax: lf_axiom (S f) Nat Nat by move => t tn; apply: Hc. split; first by apply/functionsP; saw; apply: lf_function. move => i j lij jN. have iN: natp i by apply: (NS_le_nat lij jN). rewrite ! LfV//; move: j jN lij; apply: Nat_induction. move/cle0 => ->; rewrite (Ha _ ff); exact: (cleR (CS_nat (Hu _ ff))). move => n nN Hrec; case /cle_eqVlt. by move ->; apply cleR; apply: CS_nat; apply: ax; apply: (NS_succ nN). move/(cltSleP nN) => /Hrec le1; apply: (cleT le1). by rewrite (Hb _ _ nN); apply: csum_M0le; apply: CS_nat; apply: ax. have Hv f: inc f (functions_incr r r) -> lf_axiom (D f) Nat Nat. move=> /card_increasing_Nat_aux [/functionsP [ff sf tf] fi] t tnN. rewrite /D; Ytac h; first by Wtac; rewrite sf; apply:NS0. by apply: NS_diff; rewrite /natp;Wtac; rewrite sf; apply:NS_succ. have He f: inc f (functions_incr r r) -> inc (Lf (D f) Nat Nat) fNN. by move/ Hv => aw; apply/functionsP; saw; apply: lf_function. pose D1 := fun f => (Lf (D f) Nat Nat). apply/card_eqP; exists (Lf D1 (functions_incr Nat_order Nat_order) fNN). have ns0 := NS0. saw; apply: lf_bijective. - by apply: He. - move => u v hu hv sva. move: (hu)=> /card_increasing_Nat_aux [/functionsP [fu su tu] fiu]. move: (hv)=> /card_increasing_Nat_aux [/functionsP [fv sv tv] fiv]. apply: function_exten; [ done | done | ue | ue |]. move: (Hv _ hu) (Hv _ hv) => axu axv. rewrite su; apply: Nat_induction. move: (f_equal (Vf ^~ \0c) sva); rewrite /D1 ! LfV //. by rewrite /D; Ytac0; Ytac0. move => n nN Hrec. move: (NS_succ nN) => snN. move: (f_equal (Vf ^~ (csucc n)) sva); rewrite /D1 !LfV// /D. rewrite (Y_false (@succ_nz _)) (Y_false (@succ_nz _)). rewrite (cpred_pr1 (CS_nat nN)) => eq. rewrite - (cdiff_pr (fiu _ _ (cleS nN) snN)). by rewrite - (cdiff_pr (fiv _ _ (cleS nN) snN)) eq Hrec. - move => y yf; move: (Hd y yf) => uu; ex_tac. have ax2:= (Hc y yf). move/functionsP: (yf) =>[fy sy ty]. move: (He _ uu) => /functionsP[fx sx tx]. apply:function_exten;[ done | done | by rewrite /D1;aw | by rewrite /D1;aw| ]. have ax1:= (Hv _ uu). rewrite sy => t tN; move: (NS_pred tN)=> stn. rewrite /D1 ! LfV // /D !LfV//; Ytac ww. by rewrite ww Ha. have qa: natp (Vf y t) by rewrite /natp; Wtac. have qb: natp (S y (cpred t)) by apply:ax2. move: (proj2 (cpred_pr tN ww)) => eq1. rewrite {2} eq1 (Hb _ _ stn) csumC cdiff_pr1 - ? eq1 //. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)