proposition: Lemma CR_prop0 n: natp n -> inc (CR_inv3n n) BQps.
proof: Proof. move => nN; apply: QpsS_inv; apply: QpsS_of_nat. apply: NS_pow => //; apply: NS3. apply: cpow_nz; apply: card3_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)