proposition: Lemma CR_prop00 n: natp n -> (CR_inv3n n) = \3q *q (CR_inv3n (csucc n)).
proof: Proof. move => nN. rewrite/CR_inv3n (cpow_succ _ nN) (BQprod_cN (NS_pow NS3 nN) NS3). have Hu: ratp (BQ_of_nat (\3c ^c n)). apply:QS_of_nat; apply: (NS_pow NS3 nN). rewrite(BQprod_inv Hu QS3);symmetry; apply: (BQprod_div QS3 (CR_prop1 nN)). move /pr1_def => /pr1_def; exact: card3_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)