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