proposition: Lemma nbder_0: nbder \0c = \1c.
proof: Proof. rewrite /nbder /derangements Nint_co00. set X:= Zo _ _. suff: X = singleton empty_function by move => ->; rewrite cardinal_set1. apply: set1_pr. apply/Zo_P; split; last by move => x /in_set0. apply/permutationsP; apply:empty_function_bf. move => z /Zo_P [] /Zo_P []. by rewrite functions_empty => /set1_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)