proposition: Lemma expansion_ext_aug_p1 f i (n:= expansion_value f \2c) (f' := expansion_ext_aug f i) (m:= expansion_value f' \2c): expansion_ext_of_a f n -> i<c \3c -> (n <> \0c \/ i <> \0c) -> (expansion_ext_of_a f' m /\ m = \2c *c n +c i).
proof: Proof. rewrite /m/f' /expansion_ext_aug /expansion_ext_of_a. set k := (cardinal (domain f)); rewrite Lgd. move => [[[ n3 kN lt13[fgf df fp]] nv] kp] i3 bc. set F := Lg _ _; set k1 := cardinal _. have skN:= NS_succ kN. have pa: k1 = csucc k by apply: card_nat. have pb: inc k (csucc k) by apply: Nsucc_i. have pc: exp_boundary F k1. right; split; first by rewrite pa; apply: succ_nz. rewrite pa (cpred_pr2 kN) /F LgV//; case: (equal_or_not k \0c) => kz. Ytac0; case: bc => //; rewrite - nv /expansion_value /csumb. by rewrite csum_trivial //; aw; apply: card_nonempty. by Ytac0; case: kp => // [] []. have pd: expansion_ext F k1. hnf; rewrite /F Lgd pa; split => //; split; fprops => j jb; rewrite LgV//. have jN:=(NS_inc_nat skN jb). Ytac jz => //; apply: fp; rewrite df; move:(cpred_pr jN jz) => [sa sb]. apply/(NltP kN); apply /(cltSSP (CS_nat sa)(CS_nat kN)). by rewrite - sb; apply /(NltP skN). split => //. have pe:inc \0c (Nintc k) by apply /(NintcP kN);apply: (cle0n kN). rewrite /expansion_value /F Lgd -(NintE skN) -(Nint_co_cc kN) (fct_sum_rec0 _ kN). rewrite LgV//; Ytac0; rewrite cpowx0 (cprod1r (proj31_1 i3)); congr (_ +c i). have ax: forall x, inc x (Nint k) -> inc (csucc x) (Nint1c k). move => t /(NintP kN) tk; apply/(Nint1cP kN); split; first by apply:succ_nz. by apply /(cleSltP (NS_lt_nat tk kN)). have qx: (quasi_bij csucc (Nint k) (Nint1c k)). split; first by exact. + move => u v /Nint_S1 /CS_nat cu /Nint_S1 /CS_nat cv H. by apply: csucc_inj. + move => y /(Nint1cP kN) [ynz yk];move:(NS_le_nat yk kN) => yN. move: (cpred_pr yN ynz) => [sa sb]; rewrite sb; exists (cpred y) => //. by apply /(NintP kN); apply/(cleSltP sa); rewrite - sb. rewrite (csum_Cn2 _ qx) /csumb. set G := Lg _ _. have ->: G = Lg k (fun z => (Vg f z) *c (\2c ^c (csucc z))). rewrite - (NintE kN); apply:Lg_exten => j ji /=. have ax1: inc (csucc j) (Nint1c k) by apply:ax. have ax2: inc (csucc j) (Nintc k). by move/(Nint1cP kN): ax1 => [_ h]; apply/(NintcP kN). by rewrite LgV// (Y_false (@succ_nz j)) (cpred_pr2 (Nint_S1 ji)). rewrite - nv /expansion_value cprod2Dn df; apply: csumb_exten. by move => j jk /=; rewrite (cpow_succ _ (NS_inc_nat kN jk)) cprodA cprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)