proposition: Lemma otrans_def_prop a T f: ordinalp a -> (otrans_def a T f <-> transfinite_def (ordinal_o a) T f).
proof: Proof. move => oa; rewrite / otrans_def /transfinite_def. rewrite ordinal_o_sr; split; move =>[ha hb hc]; split => // x xa. by rewrite (ordinal_segment oa xa); apply: hc; apply/(oltP oa). by move/(oltP oa): (xa) => ixa; rewrite (hc _ ixa) (ordinal_segment oa ixa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)