proposition: Lemma expansion_ext_dim_p1 f (n:= expansion_value f \2c) (f' := expansion_ext_dim f) (m:= expansion_value f' \2c) (i := Vg f \0c): expansion_ext_of_a f n -> n <> \0c -> [/\ i<c \3c, expansion_ext_of_a f' m & n = \2c *c m +c i].
proof: Proof. rewrite /m/f' /expansion_ext_dim /expansion_ext_of_a. set k := (cardinal (domain f)); rewrite Lgd. move => [[[ n3 kN lt13[fgf df fp]] nv] kp] nz. case: (equal_or_not k \0c) => knz. case nz; rewrite - nv /expansion_value; apply:csum_trivial; aw. by apply: card_nonempty. have [pkN pkv] :=(cpred_pr kN knz). have zsdf: inc \0c (domain f) by rewrite df pkv; apply/(NleP pkN); apply: (cle0n). set F := Lg _ _. have li3: i <c \3c by apply: fp. have r1:exp_boundary F (cpred k). case: kp => // ha;case: (equal_or_not (cpred k) \0c) => pkz; first by left. right; rewrite /F; move:(cpred_pr pkN pkz) => [sa sb]. move: ha => [_ ha]; split; first by rewrite sb; apply: succ_nz. rewrite LgV//; [ue | rewrite {2} sb; apply/(NleP sa); fprops]. have r2: expansion_ext F (cpred k). rewrite /F; split => //; aw; split; fprops => j ji; rewrite LgV//; apply: fp. rewrite df pkv; apply /(NleP pkN); apply /(cleSltP (NS_inc_nat pkN ji)). by apply /(NltP pkN). rewrite (card_nat pkN); split => //. rewrite - nv /expansion_value /F Lgd df - (NintE kN) {1} pkv. rewrite - (Nint_co_cc pkN). rewrite (fct_sum_rec0 _ pkN) cpowx0 (cprod1r (proj31_1 li3)); congr (_ +c i). have ax:lf_axiom csucc (Nint (cpred k)) (Nint1c (cpred k)). move => t /(NintP pkN) tk; apply/(Nint1cP pkN); split; first by apply:succ_nz. by apply /(cleSltP (NS_lt_nat tk pkN)). have qx: (quasi_bij csucc (Nint (cpred k)) (Nint1c (cpred 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 pkN) [ynz yk];move:(NS_le_nat yk pkN) => yN. move: (cpred_pr yN ynz) => [sa sb]; rewrite sb; exists (cpred y) => //. by apply /(NintP pkN); apply/(cleSltP sa); rewrite - sb. rewrite (csum_Cn2 _ qx) /csumb (NintE pkN) (NintE kN). rewrite /expansion_value cprod2Dn; apply:csumb_exten => j ji;rewrite LgV//. by rewrite (cpow_succ _ (NS_inc_nat pkN ji)) cprodA cprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)