proposition: Lemma transdef_tg0 r (f := ordinal_isog r): worder r -> forall x, inc x (substrate r) -> Vg f x = direct_image f (segment r x).
proof: Proof. move => wor x xsr. move: (transfinite_pr1 range wor) => [pa pb pc]. rewrite (pc _ xsr) dirim_restr //; rewrite pb; apply: sub_segment. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)