proposition: Lemma ord_negl_alt a b: ordinalp a -> ordinalp b -> (a <<o b <-> a *o omega0 <=o b).
proof: Proof. move => oa ob. split => lab. case: (ozero_dichot oa);first by move ->; rewrite oprod0l; apply:ole0x. move /oprod_normal=> pn; rewrite(proj2 pn _ omega_limit). apply:(ord_ub_sup ob) => t /funI_P [n nN ->]. case:(ord_negl_lt (OS_prod2 oa (OS_nat nN)) ob (ord_negl_pint nN oa ob lab)). by move => [-> _]; apply:ole0x. by case. suff hh: a <<o a *o omega0 by exact:(ord_negl_sum' oa hh lab). by rewrite /ord_negl (oprod2_nsucc oa OS_omega) (osum_int_omega olt_1omega). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)