proposition: Lemma base2r_oddK n (r := base_two_reverse) : oddp n -> r (r n) = n.
proof: Proof. move => [nN nen]; move:(NS_half nN) => hN; case: (cdouble_halfV nN) => eq. case: nen; rewrite eq; apply: (even_double hN). have nz: n <> \0c by rewrite eq; apply: succ_nz. have ox:=(base2r_oddp nN nz). move: (erefl (r n)); pose x := r n; rewrite - {1 3} /x /r. have xn: natp x by apply: NS_reverse. case: (equal_or_not x \0c) => xz. by case: (proj2 ox); rewrite -/r - /x xz; apply: even_zero. rewrite /base_two_reverse. move:(base2_expansion_prop nN nz) (base2_expansion_prop xn xz). set Fn := (the_expansion \2c n); set Fx := (the_expansion \2c x). set pn := cardinal (domain Fn); set px := (cardinal (domain Fx)). set Gn := Lg _ _; set Gx := Lg _ _. move => [[pa pb] pc pd] [[qa qb] qc qd] eq1. move:(pa) => [ha hb hc [hd he hf]]. have hi: expansion Gn \2c pn. split => //; rewrite /Gn; split; aww => i iI; rewrite LgV//. move/(NltP hb): iI => ra; move:(NS_lt_nat ra hb) => iN. have rb: csucc i <=c pn by apply /cleSltP. apply: hf; rewrite he;apply /(NltP hb). apply:(cdiff_Mlt hb hb rb); apply:(csum_M0lt hb (@succ_nz _)). have Ha:(expansion_normal_of Fx \2c px x). split => //; right; split => //; rewrite qd; fprops. have Hb:(expansion_normal_of Gn \2c pn x). have pp:inc (cpred pn) pn by apply /(NltP hb); apply: cpred_lt. have pq: expansion_of Gn \2c pn x by split; [ | symmetry]. split => //;right; split => //;rewrite /Gn LgV//. rewrite - (proj2 (cpred_pr hb pc)) cdiff_nn => bad. have [sa sb]:=(cpred_pr hb pc). move: pb; rewrite /expansion_value he sb. set t := csumb _ _ => eq2. suff: evenp t by move => eq3; case: nen; rewrite - eq2. have : forall i, i<=c (cpred pn) -> natp (Vg Fn i). move => i /(cltSleP sa); rewrite - sb => /(NltP hb). rewrite - he; move=> /hf => h; apply: (NS_lt_nat h NS2). rewrite /t; move: (cpred pn) sa; apply: Nat_induction. rewrite succ_zero csum_trivial3 bad (cprod0l). rewrite (card_card CS0); move => _; apply: even_zero. move => jk kN Hrec aux; rewrite (induction_on_sum _ (NS_succ kN)). have hw:(forall i, i <=c jk -> natp (Vg Fn i)). by move => i ij; apply: aux; apply: (cleT ij (cleS kN)). apply: (csum_of_even (Hrec hw)); rewrite - (cdouble_pow2 kN) double_prod. apply: even_double; apply: NS_prod; [ apply: aux; fprops | fprops ]. have [eq2 eq3] := (expansion_unique1 Ha Hb). rewrite - pb /expansion_value /Gx Lgd eq3 he eq2 /Gn. apply: csumb_exten => i iI. move/(NltP hb):(iI) => ra;have ra1:= (proj1 ra). have iN:=(NS_lt_nat ra hb). have rb: csucc i <=c pn by apply /cleSltP. have rc: pn -c csucc i <c pn. apply:(cdiff_Mlt hb hb rb); apply:(csum_M0lt hb (@succ_nz _)). have rd: inc (pn -c csucc i) pn by apply /(NltP hb). by rewrite !LgV // - (csucc_diff hb iN rb) double_diff. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)