proposition: Lemma order_le_compatible1 r r': worder r -> worder r' -> (r <=O r' <-> ordinal_leD1 (ordinal r) (ordinal r')).
proof: Proof. move=> wo1 wo2. move: (ordinal_o_is wo1)(ordinal_o_is wo2) => oi1 oi2. move: (OS_ordinal wo1)(OS_ordinal wo2) => o1 o2. by apply: (iff_trans (order_le_compatible oi1 oi2)); split => //; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)