proposition: Lemma expe_even n: natp n -> Nbexp(cdouble (csucc n)) = Nbexp (csucc n) +c (Nbexp n).
proof: Proof. move => nN. rewrite /Nbexp. set Ea := expansions_ext_of _. set Eb := expansions_ext_of _; set Ec := expansions_ext_of _. pose V z := (expansion_value z \2c). have Ha: forall f n, inc f (expansions_ext_of n)-> V f = n. by move => f b /Zo_hi [ [_ q] _]. have di1: disjoint Eb Ec. apply:disjoint_pr => u /Ha ua /Ha ub. by move/NatP:nN => /finite_cP [_]; rewrite - ua ub. rewrite csum2cl csum2cr - (csum2_pr5 di1). symmetry. pose F f:= expansion_ext_aug f (Yo (inc f Eb) \0c \2c). have lt23: \2c <c \3c by apply:(cltS NS2). have lt03: \0c <c \3c by apply:(clt_ltT clt_02 lt23). pose Ez f := (expansion_ext_aug f \0c). pose Et f := (expansion_ext_aug f \2c). have Hb:forall f, inc f Eb -> inc (Ez f) Ea. move => z za; move: (Ha _ _ za) => eq1;apply: expe_p3. move/Zo_hi: za; rewrite - eq1 => zb. have zc:expansion_value z \2c <> \0c \/ \0c <> \0c. left; rewrite -/(V _ )eq1; apply: succ_nz. move: (expansion_ext_aug_p1 zb lt03 zc) =>[ha]. by rewrite csum0r; fprops; rewrite /cdouble/V; move => <-. have Hc:forall f, inc f Ec -> inc (Et f) Ea. move => z za; move: (Ha _ _ za) => eq1;apply: expe_p3. move/Zo_hi: za; rewrite - eq1 => zb. have zc:expansion_value z \2c <> \0c \/ \2c <> \0c by right; fprops. move: (expansion_ext_aug_p1 zb lt23 zc) =>[ha]; rewrite -/(V z) eq1. by rewrite /cdouble (cprod_nS _ nN) => <-. have ax: lf_axiom F (Eb \cup Ec) Ea. move => f /setU2_P fa; rewrite /F; Ytac h; first by apply: Hb. by case fa => // fc;apply: Hc. have dsnz: cdouble (csucc n) <> \0c. exact (proj1(double_nz (NS_succ nN) (@succ_nz n))). pose D f :=(expansion_ext_dim f). have rax: forall f, inc f Ea -> ((Vg f \0c) = \0c /\ inc (D f) Eb) \/ ((Vg f \0c) = \2c /\ inc (D f) Ec). move => z za; move: (Ha _ _ za) => eq1. move/Zo_hi: za; rewrite - eq1 => zb. have vnz: V z <> \0c by rewrite eq1. move:(expansion_ext_dim_p1 zb vnz) => [sa sb]; rewrite -/(V z) eq1. have mN:=(NS_expe_val (proj1 (proj1 sb))). case: (equal_or_not (Vg z \0c) \0c) => ct0. rewrite ct0 (Nsum0r (NS_double mN)) => /(double_inj (NS_succ nN) mN). by move => eq; left; split => //;apply:expe_p3; rewrite eq. case: (equal_or_not (Vg z \0c) \1c) => ct1. rewrite ct1 - (Nsucc_rw (NS_double mN)) => eq2. move:(proj2 (succ_of_even (even_double mN))) (even_double (NS_succ nN)). by rewrite - eq2. case: (equal_or_not (Vg z \0c) \2c) => ct2; last first. have: Vg z \0c <c \2c by split => //;by apply/(cltSleP NS2). by move /clt2; case. rewrite /cdouble (cprod_nS _ nN) ct2. move/(csum_eq2r NS2 (NS_double nN) (NS_double mN)) /(double_inj nN mN). by move => eq; right; split => //;apply:expe_p3; rewrite eq. suff bg: bijection (Lf F (Eb \cup Ec) Ea). apply /card_eqP; apply: (equipotent_aux bg). apply: lf_bijective; first done. pose H := expansion_ext_dim_aug. move => u v us vs; rewrite /F; Ytac ub; Ytac vb => eq. + by rewrite -(H _ _ \0c ub) -(H _ _ \0c vb) eq. + case /setU2_P: vs => // vc. by rewrite -(H _ _ \0c ub) -(H _ _ \2c vc) eq. + case /setU2_P: us => // uc. by rewrite -(H _ _ \2c uc) -(H _ _ \0c vb) eq. + case /setU2_P: vs => // vc; case /setU2_P: us => // uc. by rewrite -(H _ _ \2c uc) -(H _ _ \2c vc) eq. move => y ye; move: (rax _ ye) (expansion_ext_aug_dim ye dsnz). set z := expansion_ext_dim y; case => [] [-> sb] eq. by exists z; [ apply/setU2_P; left | rewrite /F; Ytac0 ]. exists z; [ by apply/setU2_P; right | rewrite /F; Ytac hh => //;empty_tac1 z]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)