proposition: Lemma cardinal_Qps : cardinal BQps = aleph0.
proof: Proof. apply: cleA. by move: (sub_smaller BQps_sBQ); rewrite cardinal_Q. set f := Lf (fun z => (BQ_of_Z (BZ_of_nat z))) Nats BQps. have inf :injection f. apply:lf_injective; last by move => u v _ _ /pr1_def /pr1_def. move => n /setC1_P [nN nn] /=. move:(BZ_of_natp_i nN) => h1. by apply: BQ_of_Z_iQps; apply /BZps_iP; split => // /pr1_def. by move: (inj_source_smaller inf); rewrite /f; aw; rewrite cardinal_Nats. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)