proposition: Lemma symmetric_union a b: symmetricp a -> symmetricp b -> symmetricp (a \cup b).
proof: Proof. by move=> sa sb x y; case /setU2_P=> h; apply/setU2_P; [left; apply: sa | right; apply: sb ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)