proposition: Lemma ord_negl_p4 a b: a <o b -> (oopow a) <<o (oopow b).
proof: Proof. move => ltab; move:(ltab) => [[oa ob _] _]. apply/(ord_negl_alt (OS_oopow oa) (OS_oopow ob)). by rewrite - (oopow_succ oa); apply:opow_Mo_le;apply/oleSltP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)