proposition: Lemma ovaluation4 y e: ordinalp y -> ordinalp e -> ovaluation (y +o oopow e) = e.
proof: Proof. move => oy oe. by move:( ovaluation_4a oy oe PN1); rewrite (oprod1r (OS_oopow oe)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)