proposition: Theorem transfinite_definition r T: worder r -> exists! f, (transfinite_def r T f).
proof: Proof. move=> wo; apply /unique_existence. split; last by move=> x y;apply: (transfinite_unique wo). by exists (transfinite_defined r T); apply:transfinite_defined_pr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)