proposition: Lemma cnf_nr_degree x k (v := cnf_val (cnf_nr x k)): cnfp x -> k <=c domain x -> k <> \0c -> \0o <o v /\ odegree v = oexp x (cpred k).
proof: Proof. move => ox kp1 kp2. set y := (cnf_nr x k). move:(NS_le_nat kp1 (proj42 ox)) => kN. move: (cpred_pr kN kp2); set p := cpred k; move => [pN pv]. have ipkk: inc p k by rewrite pv; apply:Nsucc_i. have ->: oexp x p = oexp y p by rewrite /y /cnf_nr/oexp LgV//. have dy: domain y = csucc p by rewrite /y/cnf_nr restr_d. move: (proj44 (cnfp_cnf_nr ox kp1)); rewrite -/y dy => ax. by move:(the_cnf_p5 pN ax); rewrite - dy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)