proposition: Lemma cnf_nat_prop a: cnfp_nz a -> cnf_size a = \0c -> oexp a \0c = \0c -> (cnf_val a) <o omega0 /\ cnf_val a = ocoef a \0c.
proof: Proof. move => cnz ha hb. move:(cnf_size_nz cnz) => [qa qb]. have oda:= proj2(cnf_size_nz_ter cnz). move: (proj2 (proj44 (proj1 cnz)) _ oda)=> lp. move: (proj43 (proj1 (proj44 (proj1 cnz))) _ oda) => xf. move:(proj32_1 lp) => od. have eq0: cantor_mon omega0 (oexp a) (ocoef a) \0c = ocoef a \0c. by rewrite/cantor_mon hb opowx0 (oprod1l od). by rewrite /cnf_val/CNFbvo/CNFbv qb ha succ_zero osum_f1 eq0//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)