proposition: Lemma qsum_fusc n (p := \2c ^c n) : natp n -> qsum (fun i => fusc_quo (p +c i)) p = BQhalf (BQ_of_nat (cpred (\3c *c p))).
proof: Proof. rewrite /p; clear p; move:n; apply: Nat_induction. have eq: (fusc_quo (\1c +c \0c)) = \1q by rewrite (csum0r CS1) fusc_quo_1. rewrite cpowx0 qsum1 eq; last by apply:QS1. symmetry;rewrite (Nprod1r NS3) (cpred_pr1 CS2) /BQhalf - BQinv_2. apply: (BQprod_inv1 QS2 BQ2_nz). move => n nN Hrec. have pa := (NS_pow NS2 nN). have pb := NS_double pa. rewrite - (cdouble_pow2 nN) (qsum_even_odd pa); last first. move => i iN; exact:(QS_fusc_quo (NS_sum pb (NS_lt_nat iN pb))). rewrite {1} (qsum_fusc1 nN). set a := qsum _ _. have pN:= NS_pow NS2 nN. set b := (BQ_of_nat (\2c ^c n)). have bq: ratp b by apply:(QS_of_nat pN). set d := \3c *c \2c ^c n. have dN: natp d by apply: (NS_prod NS3 pN). have dnz: d <> \0c by apply: cprod2_nz; [ apply: succ_nz | apply: cpow2_nz]. have [cN pdv]:=(cpred_pr dN dnz). have cq:=(QS_of_nat cN). suff: a = b +q BQhalf(BQ_of_nat (cpred (\3c *c \2c ^c n))). have ha: BQhalf (\2q *q b) = b by apply: BQhalf_double. move => ->; rewrite - {2} ha /BQhalf - (BQprodDl QSh2 (QSp QS2 bq) cq). rewrite - (BQprodDl QSh2 bq (QSs (QSp QS2 bq) cq)); f_equal. rewrite (BQsumA bq (QSp QS2 bq) cq) /b -(BQprod_cN NS2 pN). rewrite (BQsum_cN pN (NS_double pN)) csumC /cdouble cprodC. rewrite - (cprod_via_sum _ CS2) cprodC (BQsum_cN (NS_prod NS3 pN) cN) cprodA. rewrite (cprodC _ \2c) - csum_nn -/d {4} pdv (csum_nS d cN). rewrite cpred_pr1; fprops. pose c1 (x:Set) := \1q. have c1p: (forall i, i <c (\2c ^c n) -> c1 i = \1q) by []. have c1r: rat_below c1 (\2c ^c n) by move => i _; apply: QS1. have cs: rat_below (fun i => fusc_quo (\2c ^c n +c i)) (\2c ^c n). move => i lin /=;move:(NS_sum pN (NS_lt_nat lin pN)) => h. exact:(QS_fusc_quo h). rewrite - Hrec /b -(qsum_one pN c1p) (qsum_sum pN c1r cs). apply: (qsum_exten pN) => i lin. have iN:=NS_lt_nat lin pN. have siN:= (NS_sum pN iN). have ssiN:= (NS_succ siN). have ha:=(QS_of_nat (NS_fusc siN)). have hb:=(QS_of_nat (NS_fusc (NS_succ siN))). have hc: BQ_of_nat (fusc (csucc (\2c ^c n +c i))) <> \0q. by move/BQ_of_nat_injective; apply: fusc_nz'. rewrite (csum_nS _ (NS_double iN)) double_sum /fusc_quo /c1. rewrite (fusc_odd siN) -(double_succ siN) (fusc_even ssiN) csumC. by rewrite (BQsum_div QS1 ha hb hc) (BQprod_1l hb) BQsum_cN //;apply:NS_fusc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)