proposition: Lemma nat_infinite_set: infinite_set nat.
proof: Proof. have zn: inc (Ro 0) nat by apply: R_inc. set g := IM (fun y:nat => J (Ro y) (Ro (S y))). have p1: sgraph g by move=> t /IM_P [a ->]; fprops. have p0: fgraph g. split => // x y /IM_P [a ->] /IM_P [b ->]; aw => sp. by rewrite sp (R_inj sp). have p2: nat = domain g. set_extens t. move=> tn; apply/(domainP p1); exists (Ro (S (Bo tn))). apply/IM_P; exists (Bo tn); by rewrite B_eq. move=> /(domainP p1) [y] /IM_P [a Je]; rewrite (pr1_def Je); apply: R_inc. have p3: range g = nat -s1 (Ro 0). set_extens t. move => /(rangeP p1) [x] /IM_P [a Jeq]. rewrite (pr2_def Jeq); apply/setC1_P; split; first by apply: R_inc. by move=> h; move:(R_inj h). move=> /setC1_P [tn to]; apply/(rangeP p1). move:(B_eq tn); move:(Bo tn) => w wv. have: w <> 0 by dneg xx; ue. rewrite -wv;clear to wv. case: w => // n _; exists (Ro n); apply/IM_P; exists n =>//. apply: (infinite_set_pr zn). exists (triple nat (nat -s1 (Ro 0)) g); saw. set f := (triple nat (nat -s1 Ro 0) g). have ff: function f by apply: function_pr => //; rewrite p3. split; last by apply:(surjective_pr1 ff); rewrite (ImfE ff) /f; aw. apply: (injective_pr_bis ff) =>// x x' y; rewrite/f; aw. move => /IM_P [a J1] /IM_P [b J2]. rewrite (pr1_def J1) (pr1_def J2). move: (pr2_def J1)(pr2_def J2)=> r3 r4. by rewrite r4 in r3; move: (R_inj r3)=> /eq_add_S ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)