proposition: Lemma wedge_inverse h (f := wedge_i1 h) (g := wedge_i2 h): inc h dexpansions -> [/\ inc f dexpansions, inc g dexpansions & (wedge f g) = h].
proof: Proof. move=> /Zo_P[/functionsP [fh sh th] [q qN qp]]. have axf: lf_axiom (fun z => Vf h (cdouble z)) Nat C2. by move => t tn /=; Wtac; rewrite sh; apply: NS_double. have axg: lf_axiom (fun z => Vf h (csucc (cdouble z))) Nat C2 by move => t tn /=; Wtac; rewrite sh; apply: NS_succ; apply: NS_double. have ft: inc f dexpansions. rewrite /f/wedge_i1; apply: Zo_i. by apply/functionsP; saw; apply: lf_function. exists q => // m mn mq; rewrite LfV// ; apply: qp; first by apply: NS_double. by apply: (cleT mq); apply: cle_n_doublen. have gt: inc g dexpansions. rewrite /g/wedge_i2; apply: Zo_i. by apply/functionsP; saw; apply: lf_function. exists q => // m mn mq; rewrite LfV//; apply: qp. by apply: NS_succ;apply: NS_double. exact:(cleT mq (cleT (cle_n_doublen mn) (cleS (NS_double mn)))). split => //. move:(wedge_exp ft gt) => /Zo_S/functionsP[fw sw tw]. apply: (function_exten fw fh); (try ue); rewrite sw => n nN. move:(NS_half nN) => hN. have ax3: lf_axiom (fun z => Yo (evenp z) (Vf f (chalf z)) (Vf g (chalf z))) Nat C2. move => t tN /=; rewrite /f/g/wedge_i1 /wedge_i1 /wedge_i2. by move:(NS_half tN) => htN; Ytac x; rewrite LfV//; [ apply: axf | apply: axg ]. rewrite /wedge LfV//. rewrite /f /g /wedge_i1 /wedge_i2=> //;Ytac hh; rewrite LfV//. by rewrite - (half_even hh). by rewrite - (half_odd (conj nN hh)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)