proposition: Lemma omega_div x: ordinalp x -> exists a b, [/\ ordinalp a, b<o omega0, x = omega0 *o a +o b & (osuccp x <-> b <> \0o)].
proof: Proof. move => ox; move: (oquoremP ox olt_0omega) => ha. move: (ha) => [oq or xv ro]. exists (oquo x omega0), (orem x omega0). have op: ordinalp (omega0 *o (oquo x omega0)) by fprops. split => //;split. move => osx rz. move: osx; rewrite xv rz (osum0r op) => osx. move/(oprod_succP OS_omega oq): osx => [so _]. case:(limit_nonsucc' omega_limit so). move => rz. rewrite xv; apply/(osum_succP op or); right. move/oltP0: ro => [_ _ rN]. move: (cpred_pr rN rz); set c := cpred _; move => [cN ->]. rewrite (succ_of_nat cN); exists c => //; exact:(OS_nat cN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)