proposition: Lemma expe_odd n: natp n -> Nbexp(csucc (cdouble n)) = Nbexp n.
proof: Proof. move => nN. have lt1: \1c <c \3c. rewrite - succ_zero; apply/(cltSSP CS0 CS2); apply: clt_02. pose F z := expansion_ext_aug z \1c. pose v f := expansion_value f \2c. have ha: forall f, expansion_ext_of_a f (v f) -> (expansion_ext_of_a (F f) (v (F f)) /\ (v (F f)) = \2c *c (v f) +c \1c). move => f h; apply: expansion_ext_aug_p1 => //; right; fprops. symmetry; apply /card_eqP; set E1 := _ n; set E2 := _ (csucc _). have ax: lf_axiom F E1 E2. move => f /Zo_hi h. have nv: n = v f by rewrite /v; move: h => [ [_ ->] _]. have hb: expansion_ext_of_a f (v f) by rewrite - nv. have [sa sb]:=(ha _ hb). move: sa; rewrite sb - nv - (Nsucc_rw (NS_double nN)); apply:expe_p3. pose G := expansion_ext_dim. suff: (bijection (Lf F E1 E2)) by apply: equipotent_aux. apply: lf_bijective; first done. rewrite /F;move => f1 f2 /(expansion_ext_dim_aug \1c) {2} <-. by move /(expansion_ext_dim_aug \1c) => {2} <- ->. have dnz: (csucc (cdouble n)) <> \0c by apply: succ_nz. move => y ye2; move:(expansion_ext_aug_dim ye2 dnz) => sa. move/Zo_hi: ye2 => sb. have h: (expansion_value y \2c) = csucc (cdouble n) by move:sb => [ [_ ->] _]. rewrite - h in sb dnz. have [ua ub]:= (expansion_ext_dim_p1 sb dnz). move:(NS_expe_val (proj1(proj1 ub))); set m := _ _ \2c; rewrite h => na nb. move:(succ_of_even (even_double nN)); rewrite nb; move => [_ nes]. move/(csum_of_evenP (even_double na) (NS_lt_nat ua NS3)):nes => ne1. have: Vg y \0c <c \2c. split; first by apply/(cltSleP NS2). move => un2;case:ne1; rewrite un2; apply: even_two. move /clt2; case; first by move => un2;case:ne1; rewrite un2; apply: even_zero. move => eq1. move: (nb); rewrite eq1 (Nsucc_rw (NS_double nN)). move/(csum_eq2r NS1 (NS_double nN) (NS_double na)) /(double_inj nN na) => eq2. rewrite eq1 in sa; rewrite -/m - eq2 in ub. exists (expansion_ext_dim y) => //;apply:(expe_p3 ub). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)