proposition: Lemma ord_powa_pr0 r r': worder r -> worder r' -> ordinal (olexp r r') = (ordinal r) ^O (ordinal r').
proof: Proof. move => wor wor'. move: (OS_ordinal wor)(OS_ordinal wor') => o1 o2. apply: ordinal_o_isu2. - by apply olexp_worder. - by apply: OS_ord_powa. move: (ordinal_o_is wor) (ordinal_o_is wor') => is1 is2. move: (ordinal_o_wor o1) => wor1. move: (ordinal_o_wor o2) => wor2. move: (opowa_invariant wor wor1 wor' wor2 is1 is2). move: (ordinal_o_is (olexp_worder wor1 wor2)) => t1 t2. by move: (orderIT t2 t1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)