proposition: Lemma cnf_sum_rec x: cnfp_nz x -> cnf_val x = cnf_val (cnf_ns x \1c) +o (oopow (oexp x \0c)) *o (ocoef x \0c).
proof: Proof. move => xnz. have od1:= proj2(cnf_size_nz_ter xnz). move: (proj44 (proj1 xnz)) => [[_ qb qc _] _]. move: (OS_oopow (qb _ od1))(proj31_1 (qc _ od1))=> ra rb. have odx: \1c <=c (domain x) by apply/cge1P. rewrite -(cnf_sum_prop3 (proj1 xnz) odx). rewrite {2}/cnf_val /cnf_nr restr_d /CNFbvo /CNFbv. set u := cantor_mon _ _ _. have eq1: u \0c = oopow (oexp x \0c) *o ocoef x \0c. rewrite/u/cantor_mon/ocoef/oexp LgV//; apply: set1_1. by rewrite osum_f1 eq1 //; apply: OS_prod2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)