proposition: Lemma oleT_si a b: ordinalp a -> ordinalp b -> (sub a b \/ inc b a).
proof: Proof. move=> oa ob; case: (oleT_el oa ob); first by move => [_ _]; left. by move/olt_i; right. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)