proposition: Lemma ord_negl_p5 e c e' c': c <o omega0 -> e <o e' -> \0o <o c' -> ((oopow e) *o c) <<o ((oopow e') *o c').
proof: Proof. move /(oltP OS_omega) => cN ltee' cnz. have oc:= (OS_nat cN). have oc':= proj32_1 cnz. move:(OS_oopow (proj31_1 ltee')) (OS_oopow (proj32_1 ltee')) => ooe ooe'. apply:(ord_negl_prod (OS_prod2 ooe oc) ooe' cnz). exact:(ord_negl_pint cN ooe ooe' (ord_negl_p4 ltee')). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)