proposition: Lemma opow_regular a b c: \2o <=o a -> ordinalp b -> ordinalp c -> a ^o b = a ^o c -> b = c.
proof: Proof. move=> h ob oc. case: (oleT_ell ob oc) => //h1; move: (opow_Meqlt h h1) => [_ h2] //. by move=> h3; case: h2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)