proposition: Lemma Exercise6_33g : bijection_prop E6_33_x c M.
proof: Proof. apply:equipotent_ex_pr; apply/card_eqP. by rewrite Exercise6_33f (card_card (proj1 Exercise6_33c)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)