proposition: Lemma ovaluationE e c n (x:= CNFbvo e c (csucc n)): natp n -> CNFb_axo e c (csucc n) -> ovaluation x = e \0c.
proof: Proof. move => nN ax. move:(CNFq_pg5 nN ax) => xp. rewrite /x /ovaluation (the_cnf_p3 ax (NS_succ nN)). by rewrite /oexp LgV //; aw;trivial; apply/(NleP nN); apply: cle0n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)