proposition: Lemma qsum_fusc1 n (p := \2c ^c n) : natp n -> qsum (fun i => fusc_quo ( (cdouble p) +c (cdouble i))) p = BQhalf (BQ_of_nat p).
proof: Proof. move => nN; case: (equal_or_not n \0c) => nz. have eq: (fusc_quo (cdouble \1c +c cdouble \0c)) = \2hq. by rewrite cdouble0 /cdouble (cprod1r CS2) (csum0r CS2) fusc_quo_2. by rewrite /p nz cpowx0 /BQhalf (BQprod_1l QSh2) qsum1 eq //; apply: QSh2. move:(cpred_pr nN nz) => [sa sb]. set q := \2c ^c (cpred n). have pv: p = cdouble q by rewrite /p sb cdouble_pow2. have pN: natp p by apply: (NS_pow NS2 nN). have qN: natp q by apply: (NS_pow NS2 sa). have tnz: BQ_of_nat \2c <> \0q by move /BQ_of_nat_injective; fprops. have ha:forall i, i <c q +c q -> inc (fusc_quo (cdouble (p +c i))) BQ. move => i iq; move:(NS_double(NS_sum pN (NS_lt_nat iq (NS_sum qN qN)))) => h. exact (QS_fusc_quo h). have hb: forall i, i <c q -> inc (fusc_quo (cdouble (p +c (q +c i)))) BQ. move => i iq; move:(NS_double(NS_sum pN (NS_sum qN(NS_lt_nat iq qN)))) => h. exact (QS_fusc_quo h). transitivity (qsum (fun i => fusc_quo (cdouble (p +c i))) p). by apply:(qsum_exten pN) => i lip; rewrite double_sum. have hc: forall i, i <c q -> inc (fusc_quo (cdouble (p +c i))) BQ. by move => i iq; apply: ha; apply: (clt_leT iq); apply: csum_M0le; fprops. have hd: forall i, i<c q -> inc (fusc_quo (cdouble (p +c (q +c (q -c csucc i))))) BQ. move => i iq;move: (NS_sum pN (NS_sum qN (NS_diff (csucc i) qN))) => h. exact (QS_fusc_quo (NS_double h)). rewrite {2 3} pv BQhalf_prop (BQprod_cN NS2 qN) {2} /cdouble - csum_nn. rewrite (BQdiv_prod (QS_of_nat NS2) (QS_of_nat qN) tnz) (qsum_An qN qN ha). rewrite [X in _ +q X] (qsum_rev qN hb) (qsum_sum qN hc hd); apply:(qsum_one qN). move => i liq. have iN:=(NS_lt_nat liq qN). have pa:= (NS_sum pN iN). have qq: q +c q = p by rewrite csum_nn -/(cdouble q) - pv. have ra: p <=c p +c i by apply: csum_M0le; fprops. have ra' :=(cleT ra (cleS pa)). have sd: q <=c p by rewrite - qq; apply:(csum_M0le _ (CS_nat qN)). have leip := (cleT (proj1 liq) sd). move/(cleSltP iN): liq => iq. have se := (cleT iq sd). rewrite (csumC q) -(cdiffA2 qN qN iq) qq. have sc: natp (p +c (p -c csucc i)) by apply:(NS_sum); fprops. have rb': csucc (p +c i) <=c cdouble p. by rewrite /cdouble - csum_nn - (csum_nS _ iN); apply:(csum_Meqle). have rb:= (cleT (cleS pa) rb'). have rc: p <=c csucc (p +c (p -c csucc i)). by apply: cleT (cleS sc);apply: csum_M0le; fprops. have rc': p <=c (p +c (p -c csucc i)) by apply: csum_M0le; fprops. have rd: csucc (p +c (p -c csucc i)) <=c cdouble p. apply /(cleSltP sc);rewrite /cdouble - csum_nn; apply:(csum_Meqlt pN). apply:(cdiff_Mlt pN pN se (csum_M0lt pN (@succ_nz i))). have rd':= cleT (cleS sc) rd. have rj: (p +c (p -c csucc i)) +c (p +c (csucc i)) = \3c *c p. rewrite (csumC _ (csucc i)) csumA - (csumA p) (csumC _ (csucc i)) cdiff_pr //. by rewrite/ card_three csum_nn cprodC - (cprod_nS _ NS2) cprodC. have re: (p +c i) +c csucc (p +c (p -c csucc i)) = \3c *c p. by rewrite csumC(csum_Sn _ sc) -(csum_nS _ (NS_sum pN iN)) -(csum_nS _ iN) rj. have re': csucc (p +c i) +c (p +c (p -c csucc i)) = \3c *c \2c ^c n. by rewrite csumC - (csum_nS _ iN). rewrite /fusc_quo (fusc_even pa)(fusc_odd pa)(fusc_even sc)(fusc_odd sc). rewrite -(fusc_palindrome nN ra rb rc rd re). rewrite -(fusc_palindrome nN ra' rb' rc' rd' re') (csumC _ (fusc (p +c i))). have ua: natp (fusc (p +c i)) by apply:NS_fusc. have ub: natp (fusc (csucc (p +c i))) by apply:NS_fusc; apply: NS_succ. rewrite - (BQsum_cN ua ub). set a := BQ_of_nat _; set b := BQ_of_nat _. have aq: ratp a by apply:QS_of_nat. have bq: ratp b by apply:QS_of_nat. rewrite /BQdiv - (BQprodDl (QS_inv (QSs aq bq)) aq bq). apply: (BQdiv_xx (QSs aq bq)); rewrite /a/b (BQsum_cN ua ub) - (fusc_odd pa). move/BQ_of_nat_injective; apply: (fusc_nz' (NS_double pa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)