proposition: Lemma fusc_quo_pow2 n: natp n -> fusc_quo (\2c ^c n) = BQinv (BQ_of_nat (csucc n)).
proof: Proof. move => nN; rewrite /fusc_quo. have pN: natp (\2c ^c n) by fprops. rewrite (Nsucc_rw pN) (fusc_succ_pow2 nN) (fusc_pow2 nN). by rewrite (BQdiv_1x (QS_of_nat (NS_succ nN))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)