proposition: Lemma wedge_i2p f g: inc f dexpansions -> inc g dexpansions -> wedge_i2 (wedge f g) = g.
proof: Proof. move=> /Zo_P[/functionsP [ff sf tf] [bf bfN bfp]]. move=> /Zo_P[/functionsP [fg sg tg] [bg bgN bgp]]. rewrite /wedge; set h := fun _ => _. have ax: lf_axiom h Nat C2. rewrite /h => z zn /=; Ytac w; Wtac. by rewrite sf; apply: NS_half. by rewrite sg; apply: NS_half. have ax2: lf_axiom (fun z => Vf (Lf h Nat C2) (csucc (cdouble z))) Nat C2. by move => x xN /=;move:(NS_succ(NS_double xN)) => dN; rewrite LfV//; apply: ax. apply: function_exten => //. - by apply/lf_function. - by rewrite/wedge_i2; aw. - by rewrite/wedge_i2; aw. - rewrite/wedge_i2; aw=> a aN;move:(NS_succ (NS_double aN)) => dN; rewrite !LfV//. by rewrite /h (Y_false (proj2 (odd_succ_double aN)))(odd_half aN). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)