proposition: Lemma CNF_succ_pow1 n c (x := (osucc ((oopow n) *o c))) (X := variantLc (J \0o \1o) (J n c)): \0o <o n -> posnatp c-> cnf_and_val X x.
proof: Proof. move => ha hb. move/posnat_ordinalp: (hb) => /proj1 /proj32_1 on. move:(cnf_two_terms ha hb PN1); rewrite /oopow opowx0 (oprod1r OS1). rewrite osucc_pr //; apply: (OS_prod2 (OS_oopow (proj32_1 ha)) on). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)