proposition: Lemma oltP0 x y: x <o y <-> [/\ ordinalp x, ordinalp y & inc x y].
proof: Proof. split. by move=> [[ox oy sxy] nxy]; split => //; case: (ordinal_sub ox oy sxy). by move=> [ox oy xy]; move: (ordinal_sub2 oy xy) => [pa pb]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)