proposition: Lemma oleSltP a b: a <o b <-> (osucc a) <=o b.
proof: Proof. split. by move => h; apply :(proj2 (osucc_pr0 (proj31_1 h))). move => [pa pb pc]; have asa:= (pc _ (setU1_1 a a)). apply /oltP0;split => //; exact:(Os_ordinal pb asa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)