proposition: Lemma shift_p1 f: inc f dexpansions -> inc (shift f) dexpansions /\ size (shift f) = cpred (size f).
proof: Proof. move => fd. move:(size_p fd); set fs:= size _; move =>[sfa sfb sfc]. 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 sd: inc (shift f) dexpansions. apply: Zo_i. by rewrite/shift;apply/functionsP; saw; apply: lf_function. rewrite/shift; exists q => // m mN lmn; rewrite !LfV//. move:(NS_succ mN). move:(cleT lmn (cleS mN)) => ra rb. by apply: qp. move:(size_p sd); set s := size _; move =>[sa sb sc]; split => //. have aux2: fs <=c s -> s = \0c. move => le; case: sc => // - [pN pv]; rewrite /shift LfV// pv. case; exact:(sfb _ sa le). case: sfc. by move => sfz; rewrite sfz cpred0; apply: aux2; rewrite sfz; apply:cle0n. set r := cpred fs; move =>[rN rv fv]. case:(NleT_ell sa rN) => // csr. case:(equal_or_not r \0c) => rz. by case: (nesym (proj2(cle_ltT (cle0n sa) csr))). move:(cpred_pr rN rz) => [mN mv]. move: csr; rewrite mv; move/(cltSleP mN) => le1. case: fv; move:(sb _ mN le1); rewrite /shift LfV//; ue. case:(equal_or_not s \0c) => sz. by case: (nesym (proj2(cle_ltT (cle0n rN) csr))). by move/(cleSltP rN): csr; rewrite rv => /aux2. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)