proposition: Lemma setX_rS x y y': nonempty x -> sub (x \times y) (x \times y') -> sub y y'.
proof: Proof. by move=> [t tx] s z zy; move: (s _ (setXp_i tx zy)); case/setXp_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)