proposition: Lemma shift_val f: inc f dexpansions -> value f = Vf f \0c +c \2c *c (value (shift f)).
proof: Proof. move => fd. move:fd=> /Zo_P [/functionsP[ff sf tf] [q qN qp]]. have ax: lf_axiom (fun z => Vf f (csucc z)) Nat C2. move => t /NS_succ tN; Wtac; ue. have qb: quasi_bij csucc Nat (Nat -s1 \0c). split. - by move => t tn; apply/setC1_P; split; [ apply: NS_succ | apply: succ_nz]. - by move => u v /CS_nat cu /CS_nat cv; apply: csucc_inj. - move => y /setC1_P [yN ynz]; move:(cpred_pr yN ynz)=> [qa qb]. by exists (cpred y). rewrite {2} /value cprod2Dn; set s1 := csumb _ _. pose g i := (Vf f i *c \2c ^c i). have ->: s1 = csumb Nat (fun i => g (csucc i)). apply: csumb_exten => i iN. by rewrite /shift /g LfV//; rewrite cprodC - cprodA cpow_succ. have hu: ~ inc \0c (Nat -s1 \0c) by case/setC1_P. have hv: ((Nat -s1 \0c) +s1 \0c) = Nat by apply: setC1_K; apply: NS0. have ->: Vf f \0c = g \0c. rewrite /g cpowx0 cprod1r //; apply: CS_nat;apply:(NS_inc_nat NS2). rewrite- [\2c] / C2; Wtac; rewrite sf; apply:NS0. rewrite -(csum_Cn2 g qb) csumC - csumA_setU1//; ue. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)