proposition: Lemma cardinal_Q : cardinal BQ = aleph0.
proof: Proof. move/infinite_setP: infinite_Nat => icn. have hb:= cardinal_BZ. set f := Lf BQ_of_Z BZ BQ. apply: cleA. move /sub_smaller: BZps_sBZ; rewrite hb => c2. have /sub_smaller: sub BQ (BZ \times BZ). by move => t /Zo_S /setX_P [pa pb /BZps_sBZ pc]; apply/setX_P. by rewrite - cprod2_pr1 - cprod2cl - cprod2cr hb aleph0_pr3. have inf: injection f. apply: lf_injective; first by move =>z; exact: BQ_of_Z_iQ. by move => u v _ _ /pr1_def. by move: (inj_source_smaller inf); rewrite /f; aw; rewrite hb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)