proposition: Lemma oltP a: ordinalp a -> forall x, (x <o a <-> inc x a).
proof: Proof. move=> oa x; split; first by apply:olt_i. move => xa; apply/oltP0; split => //; exact:(Os_ordinal oa xa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)