proposition: Lemma ovaluation_opow n: ordinalp n -> ovaluation (oopow n) = n.
proof: Proof. move => on. rewrite /ovaluation (proj43(cnf_singleton1 on)) /oexp LgV//; aw; trivial. by apply: set1_1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)