proposition: Lemma Exercise6_5c E: infinite_set E -> (permutations E) <=cc (\Po E).
proof: Proof. move=> isE. set C:= (functions E E). have pb: sub (Zo C bijection) C by apply: Zo_S. apply: (cleT (sub_smaller pb)). apply: (cleT (Exercise6_5a E E)). case: (emptyset_dichot E) => neE. move: isE; rewrite neE => /infinite_setP; rewrite cardinal_set0. by move/(finite_not_infinite finite_0). have cle2: (cardinal E) <=c (cardinal E) by fprops. move: (Exercise6_5b E E) (cprod_inf3 neE cle2 isE) => ca cb. have -> : (cardinal (\Po E) = cardinal (\Po (product E E))) => //. by rewrite !card_setP - (cpowcr _ (E\times E)) cb cpowcr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)