nat_endo_uncountable.v

From Coq Require Import ssreflect ssrbool ssrfun Logic.FunctionalExtensionality.
From mathcomp Require Import ssrnat.

Definition surjection {X Y : Type} (f : X -> Y) :=
  forall y, exists x, f x = y.

Theorem nat_endomorphisms_are_uncountable :
  ~ exists (f : nat -> (nat -> nat)), surjection f.
Proof.
case=>f Hf.
case: (Hf (fun n => (f n n).+1))=>x /equal_f /(_ x) Hctra.
by move: (ltnSn (f x x)); rewrite {1}Hctra ltnn.
Qed.