proposition: Lemma transdef_tg2 r f: worder r -> surjection f -> source f = substrate r -> (forall x, inc x (substrate r) -> Vf f x = Vfs f (segment r x)) -> f = ordinal_iso r.
proof: Proof. move => wor pa pb pc. have pd: transfinite_def r target f by split => // x /pc ->; rewrite corresp_t. by move: (transfinite_pr wor pd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)