proposition: Lemma cardinal_BQ_int01: cardinal BQ_int01 = aleph0.
proof: Proof. apply: cleA; first by rewrite - cardinal_Q; apply: sub_smaller; apply: Zo_S. pose f i := (BQ_of_Zinv (BZ_of_nat (i+c \2c))). suff H : lf_axiom f Nat BQ_int01. have: injection (Lf f Nat BQ_int01). apply: lf_injective => // i j iN jN /pr2_def /pr1_def. by move /(csum_eq2r NS2 iN jN). by move/inj_source_smaller; aw; rewrite cardinal_Nat. move => i iN; move: (NS_sum iN NS2) => /BZ_of_natp_i i2N. have pa: inc (BZ_of_nat (i +c \2c)) BZps. apply/ BZps_iP;split => // /pr1_def => h. have: \2c <=c i +c \2c by apply: csum_Mle0; fprops. by rewrite h => /(cltNge clt_02). move:(BQ_of_Zi_iQps pa) => pb. move: (BQps_sBQ pb) => pc. apply:Zo_i => //; split; first by apply/ qlt0xP. split; last first. move /pr2_def /pr1_def => h. have: \2c <=c i +c \2c by apply: csum_Mle0; fprops. by rewrite h=> /(cltNge clt_12). have q1 := QS1. have q2:= BZps_sBZp ZpsS1. have sa: intp (BZ_of_nat (i +c \2c)) by apply:BZps_sBZ. have sb:= ZS1. split => //; rewrite /BQle_aux /f /BQ_of_Zinv /BQ_one /BQ_of_Z; aw. rewrite !BZprod_1r //. have h: \2c <=c i +c \2c by apply: csum_Mle0; fprops. apply /zle_P1 => //; rewrite /BZ_one /BZ_of_nat ; aw. apply: (cleT cle_12 h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)