proposition: Lemma CNF_succ_pow n (x:= osucc (oopow n)) (X := variantLc (J \0o \1o) (J n \1c)): \0o <o n -> cnf_and_val X x.
proof: Proof. move => ha; move:(CNF_succ_pow1 ha PN1). by rewrite (oprod1r (OS_oopow (proj32_1 ha))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)