proposition: Lemma cnf_one_term e c: ordinalp e -> posnatp c -> cnf_and_val (Lg \1c (fun _: Set => (J e c))) ((oopow e) *o c).
proof: Proof. move => oe pnc; set y := Lg _ _. move/posnat_ordinalp: (pnc) => [_ /proj31_1 oc]. move: (OS_prod2 (OS_oopow oe) oc)=> om. have eq1: cantor_mon omega0 (oexp y) (ocoef y) \0c = ((oopow e) *o c). by rewrite /y/cantor_mon /oexp/ocoef (LgV (set1_1 C0)); aw. have <-: cnf_val y = ((oopow e) *o c). by rewrite /cnf_val /CNFbvo /CNFbv {3} /y Lgd osum_f1 eq1. apply: cnf_and_val_pb; rewrite/y; apply/cnfpP; split. - fprops. - aww. - aw => i i1; rewrite LgV//; split => //; aww; by apply: PN1. - by aw; move => i /CS_nat iN; rewrite - succ_zero; move/(cltSSP iN CS0) /clt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)