proposition: Lemma otrans_defined_pr a T: ordinalp a -> otrans_def a T ( otrans_defined a T).
proof: Proof. move => ox; apply/(otrans_def_prop _ _ ox). apply: (transfinite_defined_pr _ (ordinal_o_wor ox)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)