proposition: Lemma ovaluation_4a x e c: ordinalp x -> ordinalp e -> posnatp c -> ovaluation (x +o (oopow e) *o c ) = e.
proof: Proof. move => ox oe cp. move: (cnf_one_term oe cp) =>[]; set b := Lg _ _; set y := _ *o _. move => ob oy pa pb. move: (the_cnf_p0 ox); set a := the_cnf x; move => [oa vv]. have hu: oexp b \0c = e. by rewrite /b/oexp LgV//; aw; trivial;exact: (set1_1 \0c). have db: domain b = \1c by rewrite /b Lgd. by rewrite /ovaluation (cnf_osum ox oy) -/a pa cnf_valuation_sum_spec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)