proposition: Lemma ovaluation7 e x e' x' : ordinalp e -> ordinalp e' -> osuccp x -> osuccp x' -> oopow e *o x = oopow e' *o x' -> (e = e' /\ x = x').
proof: Proof. move => oe oe' [y oy ->] [y' oy' ->]. move:(OS_pow OS_omega oe) (OS_pow OS_omega oe') => op op' => eq1. move: (eq1);rewrite (oprod2_succ op oy) (oprod2_succ op' oy') => eq2. move:(f_equal ovaluation eq2). rewrite (ovaluation4 (OS_prod2 op oy) oe). rewrite (ovaluation4 (OS_prod2 op' oy') oe') => ee'. rewrite ee' in eq1;split => //. apply:(oprod2_simpl (OS_succ oy) (OS_succ oy') (oopow_pos oe') eq1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)