proposition: Lemma nat_fun_function: function nat_fun.
proof: Proof. have cf: correspondence nat_fun. apply: corresp_create => x /IM_P [a ->]. by apply /setXp_P; split; apply: R_inc. have sf: source nat_fun = nat by rewrite /nat_fun; aw. have tf: target nat_fun = nat by rewrite /nat_fun; aw. split => //. split; first by move => x /nat_map_P [n ->]; fprops. by move => x y /nat_map_P [n ->]/nat_map_P [m ->]; aw=> eq; rewrite(R_inj eq). rewrite sf; set_extens t. move => [a <-]; apply/funI_P;exists (J (Ro a)(Ro a.+1)); aw; trivial. by apply/nat_map_P; exists a. move/funI_P => [z /nat_map_P [a ->] ->]; aw; apply: R_inc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)