proposition: Lemma fusc_sum_simpl n (p := \2c ^c n): natp n -> fsimpl_sum p p = \1q.
proof: Proof. move => nN; case: (equal_or_not n \0c) => nz. set a := (BQ_of_nat (fusc (\1c +c \0c) *c fusc (\1c +c csucc \0c))). have aux: BQinv a = \1q. rewrite /a succ_zero (Nsum0r NS1) csum_11 fusc1 fusc2. by rewrite (cprod1r CS1) BQinv_1. rewrite /p nz cpowx0 /fsimpl_sum qsum1 aux //; apply: QS1. move: (cpred_pr nN nz) => [sa sb]. rewrite /p sb - (cdouble_pow2 sa); set q:= (\2c ^c cpred n). have qN: natp q by apply: (NS_pow NS2 sa). have pv: p = cdouble q by rewrite /p sb cdouble_pow2. have qq: q +c q = p by rewrite csum_nn -/(cdouble q) - pv. have pN: natp p by apply: (NS_pow NS2 nN). have ha: forall i, i <c q +c q -> inc (BQinv (BQ_of_nat (fusc (p +c i) *c fusc (p +c csucc i)))) BQ. rewrite qq => i lin; move:(NS_lt_nat lin pN) => h. apply:QS_inv; apply: QS_of_nat; apply: NS_prod; apply:NS_fusc; fprops. have hb: forall i, i <c q -> inc (BQinv (BQ_of_nat (fusc (p +c (q +c i)) *c fusc (p +c csucc (q +c i))))) BQ. move => i iq; move: (NS_lt_nat iq qN) => iN; apply:QS_inv; apply: QS_of_nat. apply: NS_prod; apply:NS_fusc; fprops. rewrite - pv - {2} qq /fsimpl_sum (qsum_An qN qN ha). rewrite -{1} /(fsimpl_sum _ _) {1} pv (fusc_rec_spec2 sa) (qsum_rev qN hb). set w := qsum _ _. suff: w = \2hq by move => ->; exact BQdouble_half2. rewrite - (fusc_rec_spec2 sa); apply: (qsum_exten qN) => i iq. have sd: q <=c p by rewrite - qq; apply:(Nsum_M0le _ qN). have leip := (cleT (proj1 iq) sd). have iN:=(NS_lt_nat iq qN);move/(cleSltP iN): iq => iq. have se := (cleT iq sd). rewrite (csumC q) -(cdiffA2 qN qN iq) qq cprodC. rewrite (csum_nS p (NS_diff (csucc i) pN)) -/ q - pv. have sc: natp (p +c (p -c csucc i)) by apply:(NS_sum); fprops. have rf: p <=c (p +c (p -c csucc i)). apply: (Nsum_M0le (p -c csucc i) pN). have ra: p <=c csucc (p +c (p -c csucc i)) by apply: (cleT rf (cleS sc)). have rb: 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 rc: \2c ^c n <=c p +c i by apply:csum_M0le; fprops. have rd: p +c i <=c cdouble p. rewrite /cdouble - csum_nn; apply:(csum_Meqle _ leip). 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: csucc (p +c (p -c csucc i)) +c (p +c i) = \3c *c p. rewrite (csum_Sn _ sc) - (csum_nS _ (NS_sum pN iN)) - (csum_nS _ iN) rj //. have rg: (p +c (p -c csucc i)) <=c cdouble p by apply: (cleT (cleS sc) rb). have rh: \2c ^c n <=c p +c (csucc i) by apply:csum_M0le; fprops. have ri: p +c (csucc i) <=c cdouble p. rewrite /cdouble - csum_nn; apply:(csum_Meqle) => //. rewrite (fusc_palindrome nN ra rb rc rd re). by rewrite (fusc_palindrome nN rf rg rh ri rj). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)