proposition: Lemma ordinal_o_o x: ordinalp x -> ordinal (ordinal_o x) = x.
proof: Proof. move=> ox; move: (ordinal_o_wor ox) => woi. have h := (ordinal_isomorphism_exists woi). exact:(esym (proj1 (ordinal_isomorphism_unique ox (OS_ordinal woi) h))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)