proposition: Lemma opow_nz0 x y: ordinalp x -> ordinalp y -> x ^o y = \0o -> (x = \0o /\ y <> \0o).
proof: Proof. move=> ox oy pz. case: (equal_or_not y \0o) => ynz. move: pz; rewrite ynz; rewrite opowx0 => h'. by case: (card1_nz). split => //. case: (equal_or_not x \0o) =>// xnz. have xp:= (ord_ne0_pos ox xnz). have yp:= (ord_ne0_pos oy ynz). move: (opow_Meqle1 xp yp); rewrite pz; apply: ole0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)