proposition: Lemma ex5_Y_prop1 J k x: ex5_upper_bd J k -> sub (ex5_Y J k x) (Vg (psE S) k).
proof: Proof. move => ha. case: (emptyset_dichot J) => Jne. rewrite /ex5_Y Jne setIf_0; apply: sub0_set. move: Jne => [i iJ] t ti. by move:(setIf_hi ti iJ); case/(ex5_Xij_pr (Vg x i) (proj2 ha _ iJ)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)