proposition: Lemma nat_fun_injective: injection nat_fun.
proof: Proof. split; first by apply:nat_fun_function. rewrite {1}/nat_fun; aw; move => x y [a <-] [b <-]. by rewrite ! nat_fun_ev => eq; rewrite (eq_add_S _ _ (R_inj eq)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)