proposition: Lemma wedge_exp f g: inc f dexpansions -> inc g dexpansions -> inc (wedge f g) dexpansions.
proof: Proof. move=> /Zo_P[/functionsP [ff sf tf] [bf bfN bfp]]. move=> /Zo_P[/functionsP [fg sg tg] [bg bgN bgp]]. have ax: lf_axiom (fun z => Yo (evenp z) (Vf f (chalf z)) (Vf g (chalf z))) Nat C2. move => z zn /=; Ytac w; Wtac. by rewrite sf; apply: NS_half. by rewrite sg; apply: NS_half. apply:Zo_i. by rewrite/wedge; apply/functionsP; saw; apply:lf_function. move: (Nmax_p1 (NS_double bfN) (NS_succ (NS_double bgN))). set c := cmax _ _; move =>[cN cp1 cp2]. exists c => // m mN lcm. rewrite /wedge LfV//. move:(NS_half mN) => hN. case:(cdouble_halfV mN) => ea. move:lcm; rewrite {1 2}ea (Y_true (even_double hN)) => ll. apply: bfp => //; apply/(double_monotone bfN hN); apply:(cleT cp1 ll). move:lcm; rewrite {1 2}ea (Y_false (proj2 (odd_succ_double hN))) => ll. have hy: cardinalp (cdouble (chalf m)) by apply:CS_nat; apply: NS_double. move/(cleSSP (CS_nat (NS_double bgN)) hy) :(cleT cp2 ll). by move/(double_monotone bgN hN) => hx;apply:(bgp _ hN). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)