proposition: Lemma nbder_1: nbder \1c = \0c.
proof: Proof. rewrite /nbder;set E := derangements _. suff: E = emptyset by move => ->; apply: cardinal_set0. apply /set0_P => t /Zo_P [] /Zo_P [] /functionsP [ff sf tf] _ pf. move:Nint_co01 => [pa pb]. move: (pf _ pa) => f0. by rewrite - sf in pa; move: (Vf_target ff pa); rewrite tf pb => /set1_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)