proposition: Lemma ordinal_o_isu1 r r': worder r -> worder r' -> r \Is r' -> ordinal r = ordinal r'.
proof: Proof. move=> w1 w2 or. move: (OS_ordinal w1)(OS_ordinal w2) => o1 o2. move: (ordinal_o_is w1)(ordinal_o_is w2) => i1 i2. exact: (ordinal_o_isu o1 o2 (orderIT (orderIT (orderIS i1) or) i2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)