proposition: Lemma Exercise6_33d: injection_prop X c (F -s1 emptyset).
proof: Proof. suff:exists f0, injection_prop f0 c (F -s1 emptyset) by apply:choose_pr. apply/eq_subset_cardP1. move:(cle_inf_inf Exercise6_33a (proj1 HF1)) => /infinite_setP iF. rewrite - (card_setC1_inf _ iF) (card_card (proj1 Exercise6_33c)). by apply/(cnext_pr5P (proj31_1 HF1)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)