proposition: Lemma cnf_two_terms n1 c1 n2 c2 (x := (oopow n1 *o c1) +o (oopow n2 *o c2)) (X := variantLc (J n2 c2) (J n1 c1)): n2 <o n1 -> posnatp c1 -> posnatp c2 -> cnf_and_val X x.
proof: Proof. move=> ha hb hc. move:(ha) => [[oe2 oe1 _] _]. have <-: cnf_val X = x. rewrite /X/cnf_val/CNFbvo/CNFbv; aw; rewrite - [C2] succ_one. rewrite (osum_fS _ NS1) /cantor_mon/ocoef/oexp LgV//; aww. - rewrite - succ_zero (osum_fS _ NS0) osum_f0 LgV//;aww. move/posnat_ordinalp: hc => [_ /proj31_1 oc2]. by rewrite (osum0r (OS_prod2 (OS_oopow oe2) oc2)). apply: cnf_and_val_pb;rewrite/X; apply/cnfpP; split. - fprops. - aw; apply: NS2. - aw => i i2; try_lvariant i2; split; aww. - aw => i iN; rewrite -[C2] succ_one; move/(cltSSP (CS_nat iN) CS1). by move/clt1 => ->; rewrite /oexp succ_zero; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)