proposition: Lemma ordinal_same_wo x: ordinalp x -> ordinal_o x = ordinal_oa x.
proof: Proof. move=> ox; rewrite - ordinaloa_alt; apply: graph_on_exten => a b ax bx. move:(Os_ordinal ox ax) (Os_ordinal ox bx) => oa ob. exact :ordinal_sub4P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)