proposition: Lemma universe_trans a: ordinalp a -> transitive_set (universe a).
proof: Proof. pose p x := transitive_set (universe x). apply: (least_ordinal2 (p:=p)) => y oy h t. move /(universe_P oy) => [s sy sb]. move => b bt; apply /(universe_P oy);exists s => //;apply:(h _ sy _ (sb _ bt)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)