proposition: Lemma limit_ordinal_P4 x: ordinalp x -> (limit_ordinal x <-> exists2 y, \0o <o y & x = omega0 *o y).
proof: Proof. move => ox; split => h. move: (omega_div ox) => [a [b [oa ob dv etc]]]. case: (equal_or_not b \0o) => bz. have xa: x = omega0 *o a by rewrite dv bz osum0r; fprops. case: (ozero_dichot oa) => az; last by exists a. by case: (limit_nz h); rewrite xa az oprod0r. by move /etc: bz => sp; case(limit_nonsucc' h sp). move: h => [y [[_ oy _] ynz] ->]. move: OS_omega omega_limit => oo ol. case: (ordinal_limA oy) => hx; first by case: ynz. move: hx => [z oz zv]. rewrite zv (oprod2_succ oo oz); apply:osum_limit; fprops. apply: oprod_limit => //; apply: olt_0omega. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)