proposition: Lemma fusc_rec_spec2 n (q := \2c ^c n)(p := cdouble q) : natp n ->fsimpl_sum p q = \2hq.
proof: Proof. move => nN. rewrite (fusc_rec_spec1 nN (cleR (CS_pow \2c n))). rewrite (fusc_pow2 nN) /cdouble cprodC - (cprod_via_sum _ CS2). by rewrite (fusc_kpow2n nN NS3) fusc3 - BQinv_2 (BQdiv_1x QS2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)