proposition: Lemma oleT_ell a b: ordinalp a -> ordinalp b -> [\/ a = b, a <o b | b <o a].
proof: Proof. move=> oa ob. case: (ordinal_inA oa ob) => ha. - by constructor 2; apply/oltP. - by constructor 3; apply/oltP. - by constructor 1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)