proposition: Lemma wedge_i1p f g: inc f dexpansions -> inc g dexpansions -> wedge_i1 (wedge f g) = f.
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) (cdouble z)) Nat C2. by move => x xN /=;move:(NS_double xN) => dN; rewrite LfV//; apply: ax. apply: function_exten => //. - by apply/lf_function. - by rewrite/wedge_i1; aw. - by rewrite/wedge_i1; aw. - rewrite/wedge_i1; aw=> a aN;move:(NS_double aN) => dN; rewrite ! LfV//. by rewrite /h (Y_true (even_double aN)) (even_half aN). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)