proposition: Lemma setX_Slr x x' y y': sub x x' -> sub y y' -> sub (x \times y) (x' \times y').
proof: Proof. move=> xx' yy'; apply: (@sub_trans (x \times y')); first by apply:setX_Sr. by apply: setX_Sl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)