proposition: Lemma limit_nonsucc' a: limit_ordinal a -> osuccp a -> False.
proof: Proof. move => la osa. move:(proj2(oltS (proj31 la))). by rewrite -{1} (predo_K osa) - (limit_nonsucc la). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)