proposition: Lemma the_ordinal_iso1 r : worder r -> order_isomorphism (the_ordinal_iso r) (ordinal_o (ordinal r)) r.
proof: Proof. move=> wor; exact(inverse_order_is (ordinal_isomorphism_exists wor)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)