proposition: Lemma Exercise6_5d E: infinite_set E -> (cardinal (derangements E)) <=c (cardinal (\Po E)).
proof: Proof. move => h. have : sub (derangements E) (permutations E) by apply: Zo_S. move /sub_smaller => p1. exact:(cleT p1 (Exercise6_5c h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)