proposition: Lemma transfinite_def_prop2 r T f: transfinite_def r T f -> transfiniteg_def r (T \o fgraph_to_fun) (graph f).
proof: Proof. move => [[ff sjf] hb hc]; split. - exact: (function_fgraph ff). - by rewrite domain_fg. - move => x xsr; rewrite -/(Vf _ _) (hc _ xsr) fgraph_to_fun_restr //. by rewrite hb; apply: sub_segment. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)