proposition: Lemma transitive_setP x: transitive_set x <-> sub (union x) x.
proof: Proof. split; first by move => h t/setU_P [y ty] /h; apply. move => s y yx t ty; apply: s; union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)