proposition: Lemma opow_eq_one x y : ordinalp x -> ordinalp y -> x ^o y = \1o -> (x = \1o \/ y = \0o).
proof: Proof. move => ox oy p1. case: (ozero_dichot oy) => yp; [ by right | left]. case: (ozero_dichot ox) => xp; first by move: p1; rewrite xp opow0x'. move:(opow_Meqle1 xp yp); rewrite p1 => h. by move /oge1P: xp; apply:oleA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)