proposition: Lemma ord_negl_p9 x y k: cnfp x -> cnfp_nz y -> k <=c (domain x) -> (forall i, i <c k -> oexp x i <o cnf_degree y) -> cnf_val (cnf_nr x k) <<o cnf_val y.
proof: Proof. move => ox ynz lkd hd. move:(cnf_size_nz ynz)(cnf_size_nz_bis ynz). set m := cnf_size x; move => [mN dyv] hh. have ovy := (OS_cnf_val (proj1 ynz)). have kN: natp k by apply:NS_le_nat lkd (proj42 ox). case: (equal_or_not k \0c) => knz. rewrite /ord_negl. by rewrite /cnf_nr knz {1} /cnf_val /CNFbvo/CNFbv restr_d osum_f0 osum0l. move: (cnf_nr_degree ox lkd knz) => [up ud]. move: (proj44 (proj1 ynz)); rewrite dyv => ay. move: (the_cnf_p5 mN ay); rewrite - dyv -/(cnf_val _); move =>[yp ddy]. apply: (ord_negl_p7 up yp); rewrite {1} ud ddy -/(cnf_degree y). apply: (hd _ (cpred_lt kN knz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)