proposition: Lemma transfinite_unique r T : worder r -> uniqueness (transfinite_def r T).
proof: Proof. move => wor f g fp gp. move: (transfinite_def_prop2 fp) (transfinite_def_prop2 gp) => fp' gp'. move:(transfiniteg_unique wor fp' gp') => sgr. move:(proj31 fp)(proj31 gp) => sf sg; move: (proj1 sf)(proj1 sg) => ff fg. apply: (function_exten1 ff fg sgr). by rewrite - (surjective_pr0 sf) - (surjective_pr0 sg) (ImfE ff) (ImfE fg) sgr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)