proposition: Lemma oleT_el a b: ordinalp a -> ordinalp b -> a <=o b \/ b <o a.
proof: Proof. move=> oa ob; case:(oleT_ell oa ob). - move ->; left; fprops. - by move => [h _]; left. - by right. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)