proposition: Lemma card_R: cardinal BR = \2c ^c aleph0.
proof: Proof. apply: cleA. have: sub BR (powerset BQ) by move => j /Zo_P []. by move/sub_smaller; rewrite card_setP - cpowcr cardinal_Q. by move: (inj_source_smaller CR_prop12); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)