proposition: Lemma setU2_SS A B C D : sub A C -> sub B D -> sub (A \cup B) (C \cup D).
proof: Proof. move => s1 s2; apply: sub_trans (setU2_S1 (C:=C) s2); apply: (setU2_S2 s1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)