proposition: Lemma nds_base_prop i (u := nds_base i) : natp i -> [/\ odegree u = \1c, the_cnf_lc u = (\2c ^c i) & the_cnf_rem u = i].
proof: Proof. move => iN. by case: (proj2 (the_cnf_omega_kj (conj (NS_pow NS2 iN) (cpow2_pos i)) iN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)