proposition: Lemma oltSleP a b: a <o (osucc b) <-> a <=o b.
proof: Proof. split. move /oltP0=> [p1 /OS_succr p2 p3]. by split => //; apply: ordinal_sub3. move => [p1 p2]; move/(ordinal_sub4P p1 p2) => q; apply/oltP0. split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)