proposition: Lemma value_surj x: natp x -> exists2 f, inc f dexpansions & x = value f.
proof: Proof. move: NS0 => zn nN; move:(cleR (CS_nat nN)). move: x nN {1 3} x; apply: Nat_induction. move => x /cle0 ->; pose f := (Lf (fun _ => C0) Nat C2). have ax: lf_axiom (fun _ => C0) Nat C2 by move => t _ /=; fprops. have ft: inc f dexpansions. rewrite/f;apply:Zo_i. by apply/functionsP; saw; apply: lf_function. exists \0c; [ apply: NS0 | move => y yN _ ; rewrite LfV//]. exists f => //. move:(size_p ft) => [qa qb qc]. case: qc; first by move => sz; rewrite (value_b ft) sz csumb0. move => [sz pv]; case; rewrite/f LfV//. move => n nN Hrec x /cle_eqVlt; case; last by move/(cltSleP nN); apply: Hrec. move => ->. have sN := NS_succ nN. move: (Hrec _ (cle_halfSn_n nN)) => [f fp fvv]. set r := Yo (evenp (csucc n)) C0 C1. have rc2: inc r C2 by rewrite /r; Ytac h; fprops. have xv: csucc n = r +c cdouble (chalf (csucc n)). rewrite /r; Ytac h; first by rewrite - (half_even h) Nsum0l. have hh: natp (cdouble (chalf (csucc n)))by apply: NS_double; apply: NS_half. rewrite csumC - (Nsucc_rw hh); exact: (half_odd (conj sN h)). pose g := Lf (fun z => Yo (z = \0c) r (Vf f (cpred z))) Nat C2. move/Zo_P: fp => [ /functionsP [ff sf tf] [q qa qb]]. have ax: lf_axiom (fun z => Yo (z = \0c) r (Vf f (cpred z))) Nat C2. move => z zN /=; case:(equal_or_not z \0c) => zz; Ytac0 => //. by Wtac; rewrite sf; apply: NS_pred. have gt: inc g dexpansions. apply: Zo_i. by rewrite /g;apply/functionsP; saw; apply: lf_function. exists (csucc q); fprops => m mN lemq; rewrite /g LfV//. move: (clt_leT (succ_positive q) lemq) => /proj2/nesym mz. move:(cpred_pr mN mz) => [sa sb]; Ytac0; apply: (qb _ sa). apply/(cleSSP (CS_nat qa) (CS_nat sa)); ue. have g0: Vf g \0c = r by rewrite /g LfV//; Ytac0. exists g. exact. rewrite (shift_val gt) xv fvv g0. move:(shift_p1 gt) => /proj1 /Zo_S/functionsP [fs ss ts]. do 3 apply: f_equal; apply: (function_exten ff fs); try ue. rewrite sf /shift /g => v vN; move:(NS_succ vN) => svN; rewrite !LfV//. by rewrite (Y_false (@succ_nz v)) cpred_pr2. by move => t tN /=; move:(NS_succ tN) => stN; rewrite LfV//; apply: ax. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)