proposition: Lemma equipotent_N2_N: (coarse Nat) \Eq Nat.
proof: Proof. pose g2 a := (binom (csucc a) \2c). pose mi n m := n +c (g2 (n +c m)). have g2N: forall a, natp a -> natp (g2 a). move => a aN; apply: (NS_binom (NS_succ aN) NS2). have miN: forall n m, natp n -> natp m -> natp (mi n m). move=> n m nN mN; apply: (NS_sum nN (g2N _ (NS_sum nN mN))). have ha: forall n m, natp n -> natp m -> (g2 (n +c m)) <=c (mi n m). move=> n m nN mN. apply: Nsum_Mle0; apply:(g2N _ (NS_sum nN mN)). have hc: forall n, natp n -> g2 (csucc n) = (g2 n) +c (csucc n). by move=> n nN; rewrite /g2 (binom_2plus0 (NS_succ nN)). have hb: forall n m, natp n -> natp m -> (mi n m) <c (g2 (csucc (n +c m))). move=> n m nN mN. have sN:= (NS_sum nN mN). rewrite (hc _ sN) /mi csumC; apply:(csum_Meqlt (g2N _ sN)). apply /(cltSleP sN); apply: (Nsum_M0le _ nN). exists (Lf (fun z => (mi (P z) (Q z))) (coarse Nat) Nat); hnf;saw. apply: lf_bijective; first by move => t /setX_P [_ pN qN]; apply:miN. move=> u v /setX_P [pu puN quN] /setX_P [pv pvN qvN] sm. suff ss: (P u) +c (Q u) = (P v) +c (Q v). move: sm; rewrite /mi ss => ss2. have wN:= (g2N _ (NS_sum pvN qvN)). have sp:= (csum_eq2r wN puN pvN ss2). rewrite sp in ss; apply: (pair_exten pu pv sp). apply: (csum_eq2l pvN quN qvN ss). move: (ha _ _ puN quN)(hb _ _ puN quN)(ha _ _ pvN qvN)(hb _ _ pvN qvN). rewrite sm; move=> r1 r2 r3 r4. move: (cle_ltT r1 r4)(cle_ltT r3 r2)=> r5 r6. have ls2: forall z, natp z -> \2c <=c (csucc (csucc z)). move => z zN; rewrite - succ_one - succ_zero. apply:(cleSS (cleSS (cle0n zN))). suff gi: forall x y, natp x -> natp y -> (g2 x) <c (g2 (csucc y)) -> x <=c y. move: (NS_sum puN quN) (NS_sum pvN qvN) => sun svn. apply: (cleA (gi _ _ sun svn r5)(gi _ _ svn sun r6)). move=> x y xN yN; rewrite /g2. move: (NS_succ xN) (NS_succ yN) (NS_succ (NS_succ yN)) => qa qb qc. rewrite - (binom_monotone2 NS2 qa qc card2_nz (ls2 _ xN) (ls2 _ qb)). by move /(cltSleP qb)/(cleSSP (CS_nat xN)(CS_nat yN)). move=> y yN. have g2z: g2 \0c = \0c by rewrite /g2 succ_zero (binom_bad NS1 NS2 clt_12). case: (equal_or_not y \0c) => yz. rewrite yz; exists (J \0c \0c); first exact: (setXp_i NS0 NS0). by rewrite pr1_pair pr2_pair /mi (Nsum0l NS0) g2z (Nsum0l NS0). have pc: y <c (g2 (csucc y)). rewrite (hc _ yN) (csum_nS _ yN) csumC;apply/(cltSleP (NS_sum yN (g2N _ yN))). apply: (Nsum_M0le _ yN). case: (least_int_prop2 (NS_succ yN) pc (p := fun k =>y <c (g2 k))). by rewrite g2z; move=> /clt0. set x := cpred _; move => [xN psx npx]. have bp:= (hc _ xN). have g2Nx:= (g2N _ xN). have p1: y <=c ((g2 x) +c x). by apply /(cltSleP (NS_sum g2Nx xN)); rewrite - (csum_nS _ xN) - bp. have p2: g2 x <=c y by case: (cleT_el (CS_nat g2Nx) (CS_nat yN)). move: (cdiff_pr p2); move:(NS_diff (g2 x) yN);set n:= (y -c (g2 x)). move=> nN p3;rewrite -p3 in p1. have lenx:= (csum_le2l g2Nx nN xN p1). move: (cdiff_pr lenx); move:(NS_diff n xN); set m:= (x -c n). move=> mN p4;rewrite -p4 in p3. exists (J n m); first by apply: setXp_i. by rewrite /mi pr1_pair pr2_pair csumC p3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)