proposition: Lemma Exercise3_2b: let E := \2c in let F := \4c in let s1 := gfunctions E F in let s2 :=gfunctions F E in ~ (cardinalp s1) \/ ~ (cardinalp s2).
proof: Proof. move=> E F s1 s2. case: (p_or_not_p (cardinalp s1)) => cs1; last by left. case: (p_or_not_p (cardinalp s2)) => cs2; last by right. move: (Eq_fun_set E F) (Eq_fun_set F E). move /card_eqP; rewrite -/s1 (card_card cs1) -/(F ^c E) => pa. move /card_eqP; rewrite -/s2 (card_card cs2) -/(E ^c F) => pb. move: pa pb; rewrite /E /F cpow_24 => -> /Exercise3_2a rq. by case: (proj2 clt_24). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)