proposition: Lemma trans_dec_setU x: alls x trans_dec_set -> trans_dec_set (union x).
proof: Proof. move=> alt; split. by apply: transitive_setU => y /alt []. by move=> a /setU_hi [y ay yx] aa; case: ((proj2 (alt _ yx)) _ ay). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)