proposition: Lemma card_increasing_Nat (r := Nat_order) : functions_incr r r =c functions_sincr r r.
proof: Proof. move: Nat_order_wor =>[[or _] sr]. set Q1:= functions_incr r r. set Q2:= functions_sincr r r. have Hb f: inc f Q2 <-> inc f (functions Nat Nat) /\ forall i j, i <c j -> natp j -> Vf f i <c Vf f j. split. move => /Zo_P []; rewrite sr => ha hb; split => // i j [lij nij] jN. have la: glt Nat_order i j. split=> //; apply/Nat_order_leP; split => //; apply: (NS_le_nat lij jN). move: hb => [_ _ _ fp]. by move: (fp i j la) => [/Nat_order_leP/proj33 xa xb]. move =>[qa qb]; move/functionsP: (qa) => qc. apply: Zo_i; [ ue | split => //; first ue]. move: qc =>[ff sf tf]. move => i j [/Nat_order_leP[iN jN le1] nij]. move: (qb _ _ (conj le1 nij) jN) => [qd qe]. split => //; apply/Nat_order_leP. by split => //; rewrite /natp; Wtac; rewrite sf. pose subi f:= Lf (fun i=> (Vf f i) -c i) Nat Nat. have Hi0:forall f, inc f Q2 -> [/\ (forall i, natp i -> natp (Vf f i)), (forall i j, i <c j -> natp j -> (Vf f i) <c (Vf f j)) & (forall i, natp i -> (i <=c (Vf f i)))]. move=> f /Hb [/functionsP [ff sf tf] sif]. have ha i: natp i -> natp (Vf f i) by rewrite /natp - {1} sf => isf; Wtac. split => // i iN. have sN:= NS_succ iN; have lisi := cltS iN. have hq j: j <c csucc i -> natp (Vf f j). move => ll; apply: ha; apply: (NS_lt_nat ll sN). have hr a b : a <c b -> b <c csucc i -> Vf f a <c Vf f b. move => sa sb; apply: sif => //; apply: (NS_lt_nat sb sN). by apply: (strict_increasing_prop1 sN hq hr). have Hi3:forall f, inc f Q2 -> lf_axiom (fun i => (Vf f i) -c i) Nat Nat. move=> f fQ2; move: (Hi0 _ fQ2) => [p1 p2 p3]. by move: (Hi0 _ fQ2) => [sa sb sc] o oN; apply: NS_diff; apply: p1. have Hi1:forall f, inc f Q2 -> inc (subi f) (functions Nat Nat). move=> f fQ2;apply /functionsP; rewrite /subi; hnf;saw. by apply: lf_function; apply: Hi3. have Hi2:forall f, inc f Q2 -> inc (subi f) Q1. move=> f fQ2; apply /card_increasing_Nat_aux. split; first by apply: Hi1. move: (Hi0 _ fQ2) (Hi3 _ fQ2) => [p1 p2 p3] ta. move => i j lij jN. move: (NS_le_nat lij jN) => iN. rewrite /subi !LfV//. have sN:= NS_succ jN; have lisi := cltS jN. have hq k: k <c csucc j -> natp (Vf f k). move => ll; apply: p1; apply: (NS_lt_nat ll sN). have hr a b : a <c b -> b <c csucc j -> Vf f a <c Vf f b. move => sa sb; apply: p2 => //; apply: (NS_lt_nat sb sN). by apply: (@strict_increasing_prop2 (csucc j) (Vf f) sN hq hr). set (G:= Lf subi Q2 Q1). have Hi4:function G by rewrite / G; apply: lf_function. pose addi f := Lf (fun i=> (Vf f i) +c i) Nat Nat. have pa:forall f, inc f (functions Nat Nat) -> lf_axiom (fun i => (Vf f i) +c i) Nat Nat. move=> f /functionsP [ff sf tf] t tN. apply: (NS_sum _ tN); rewrite /natp; Wtac; rewrite sf. have pa2 f: inc f (functions Nat Nat) -> inc (addi f) (functions Nat Nat). move=> fE; rewrite /addi; apply /functionsP;hnf;saw. by apply: lf_function; apply: pa. have pa3: forall f, inc f Q1 -> inc (addi f) Q2. move=> f / card_increasing_Nat_aux [fe1e2 incf]; move: (pa _ fe1e2) => ax. apply /Hb; split; first by apply:pa2. move => i j lij jN. have iN:= (NS_lt_nat lij jN). move/functionsP: fe1e2 => [ff sf yf]. have aux: natp (Vf f j)by rewrite /natp; Wtac; ue. rewrite/addi !LfV//. exact: (csum_Mlelt aux (incf _ _ (proj1 lij) jN)) lij. set (F:= Lf addi Q1 Q2). have ff: function F by apply: lf_function. have cGF: G \coP F by rewrite /G/F; split => //; aw. have cFG: F \coP G by rewrite /G/F; split => //; aw. have c1i: (G \co F = identity (source F)). apply: function_exten; aw; [fct_tac | apply: identity_f| done | | ]. by rewrite /G/F; aw. move => x xsf /=;rewrite (idV xsf); aw. rewrite corresp_s in xsf. have aQ2: inc (addi x) Q2 by apply: pa3. have xx: inc x (source (Lf addi Q1 Q2)) by aw. rewrite /F compfV// LfV// /G LfV// /addi/subi. move: (xsf) => / card_increasing_Nat_aux [/functionsP [fx sx tx] icx]. apply: function_exten; aw =>//. apply: lf_function; apply: Hi3; apply: pa3 =>//. move: (Hi3 _ aQ2)=> ta2. have H a : natp a -> natp (Vf x a) by rewrite /natp => aN; Wtac. move=> a aN /=. rewrite LfV// LfV//; first by apply: (cdiff_pr1 (H a aN) aN). move => t tN /=; apply: (NS_sum (H _ tN) tN). have c2i: (F \co G = identity (source G)). apply: function_exten; [fct_tac | fprops | by aw | by rewrite /F/G; aw | ]. rewrite /G; aw => x xQ2 /=;rewrite idV //. have qQ1: inc (subi x) Q1 by apply: Hi2. move: (xQ2) => /Hb [/functionsP [fx sx tx] icx]. have xx: inc x (source (Lf subi Q2 Q1)) by aw. rewrite compfV// LfV// /F LfV// /addi/subi. symmetry; apply: function_exten; aw; trivial. apply: lf_function; apply: pa; apply: Hi1=> //. have ta3:= (Hi3 _ xQ2). have ta2:=(pa _ (Hi1 _ xQ2)). rewrite sx => i isx; rewrite ! LfV // cdiff_rpr //. exact: (proj33 (Hi0 _ xQ2) i isx). move: (bijective_from_compose cGF cFG c1i c2i) => /proj31. by move/card_bijection; rewrite /F; aw. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)