proposition: Lemma ordinal_o_isu x y: ordinalp x -> ordinalp y -> (ordinal_o x) \Is (ordinal_o y) -> x = y.
proof: Proof. move=> ox oy [f fi]; exact:proj1 (ordinal_isomorphism_unique ox oy fi). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)