proposition: Lemma base2r_even n: natp n -> base_two_reverse (cdouble n) = base_two_reverse n.
proof: Proof. move => nN. have dN:= (NS_double nN). case: (equal_or_not n \0c) => nz; first by rewrite nz cdouble0. move:(base2_expansion_prop nN nz). move:(base2_expansion_prop dN (cprod2_nz card2_nz nz)). rewrite /base_two_reverse. set E1 := (the_expansion \2c n). set E2 := (the_expansion \2c (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 NS0 clt_02)=> []. set E3 := Lg _ _. rewrite sd (csum0r (CS_prod2 _ _)) cprodC -/(cdouble n) => qa qb. have qc: (expansion_normal_of E2 \2c p2 (cdouble n)). split => //; right; split => //; rewrite hc; fprops. have p1N: natp p1 by case: sc. have qd: (expansion_normal_of E3 \2c (csucc p1) (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. move:(expansion_unique1 qc qd)=> [qe qf]. 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 = \0c by rewrite qe /E3 LgV//; aw;trivial;Ytac0. have cp1:= CS_nat p1N. have ns1: natp (csucc p1) by apply: NS_succ. 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 qf (cdiff_pr6 p1N). apply/(NleP p1N);apply: (cdiff_le1 _ cp1). exact:(NS_inc_nat ns1 ii). rewrite qf (expansion_prop7 hh cp1) (LgV p1i) cdiff_nn qg cprod0l. rewrite csum0r; last by rewrite /expansion_value /csumb; fprops. rewrite /expansion_value /restr !Lgd;apply:csumb_exten. move => 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)