proposition: Lemma nat_fun_surjective: ~ surjection nat_fun.
proof: Proof. case; rewrite {2 3} /nat_fun; aw => _ H. move: (H _ (R_inc 0)) => [x [n <-]]. by rewrite nat_fun_ev => eq; move:(R_inj eq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)