proposition: Lemma base2r_odd n: natp n -> base_two_reverse (csucc (cdouble n)) = \2c ^c (clog2 n) +c base_two_reverse n.
proof: Proof. move => nN. have dN:= (NS_double nN). case: (equal_or_not n \0c) => nz. rewrite nz cdouble0 succ_zero base2r_one base2r_zero clog0. by rewrite cpowx0 (csum0r CS1). move:(base2_expansion_prop nN nz). move:(base2_expansion_prop (NS_succ dN) (@succ_nz _)). rewrite /base_two_reverse. set E1 := (the_expansion \2c n). set E2 := (the_expansion \2c (csucc (cdouble n))). set p1:= (cardinal (domain E1)); set p2 := (cardinal (domain E2)). move => [[sa sb] hb hc] [[sc sd] hf hg]. move: (expansion_prop8_rev sc NS1 clt_12)=> []. set E3 := Lg _ _. rewrite sd cprodC -/(cdouble n) - (Nsucc_rw dN) => qa qb. have qc: (expansion_normal_of E2 \2c p2 (csucc (cdouble n))). split => //; right; split => //; rewrite hc; fprops. have p1N: natp p1 by case: sc. have qd: (expansion_normal_of E3 \2c (csucc p1) (csucc (cdouble n))). split => //; right; split => //; first by apply:succ_nz. have p1i: inc p1 (csucc p1) by apply: Nsucc_i. rewrite (cpred_pr2 p1N) /E3 LgV // (variant_false _ _ hf)hg; fprops. have [qe qf]:=(expansion_unique1 qc qd). have zi: inc \0c (csucc p1) by apply/(NleP p1N); apply:(cle0n p1N). have p1i: inc p1 (csucc p1) by apply/(NleP p1N); fprops. have qg: Vg E2 \0c = \1c by rewrite qe /E3 LgV//; aw;trivial;Ytac0. have cp1:= CS_nat p1N. have ns1:=(NS_succ p1N). have hh: expansion (Lg (csucc p1) (fun z => Vg E2 (csucc p1 -c csucc z))) \2c (csucc p1). move: sa => [q1 q2 q3 [q4 q5 q6]]; split => //; split; aww. move => i ii; rewrite LgV//; apply: q6; rewrite q5. rewrite qf (cdiff_pr6 p1N (NS_inc_nat ns1 ii)). apply/(NleP p1N);apply: (cdiff_le1 _ cp1). rewrite qf (expansion_prop7 hh cp1) (LgV p1i) cdiff_nn qg csumC. rewrite (cprod1l (CS_pow _ _)) (log2_pr2 nN); apply:f_equal. rewrite /expansion_value /csumb; apply: f_equal; aw. apply:Lg_exten => // i ii. have iN:= NS_inc_nat p1N ii. move/(NltP p1N): (ii) => lip. have sip1: csucc i <=c p1 by apply/(cleSltP iN). have ha: inc (p1 -c i) (csucc p1). apply/(NleP p1N);apply: (cdiff_le1 _ cp1). have isp: inc i (csucc p1) by rewrite (succ_of_nat p1N); apply:setU1_r. rewrite !LgV// (cdiff_pr6 p1N iN) qe - (cdiff_A1 p1N iN sip1) /E3 LgV//. by rewrite (variant_false _ _ (cdiff_nz lip)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)