proposition: Lemma limit_ordinal_P x: limit_ordinal x <-> (\0o <o x /\ forall t, t <o x -> osucc t <o x).
proof: Proof. split. move => lx; split; first by apply: limit_pos. move:lx => [ox xnz xl]. by move => t /(oltP ox) => h; apply/(oltP ox); apply: xl. move =>[[sa xnz] sb];move: (proj32 sa) => ox; split => //. exact: (olt_i (ord_ne0_pos ox (nesym xnz))). by move => t /(oltP ox) h; apply/(oltP ox); apply: sb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)