proposition: Lemma the_ordinal_iso2 r g: worder r -> order_isomorphism g (ordinal_o (ordinal r)) r -> g = the_ordinal_iso r.
proof: Proof. move =>wor; move: (the_ordinal_iso1 wor) => is1 is2. by rewrite (iso_unique_bis wor is1 is2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)