proposition: Lemma nds_k_of_bd n: 1 <n -> 0 < nds_k_of n < n.
proof: Proof. rewrite /nds_k_of. case: (ltnP 8 n); last by case: n => //; case => // n /=; rewrite ltnS. case: eqP; [by move -> | case: eqP ; [ by move -> | ]]. by case: eqP; [by move -> | move => _ _ _ /= n8 _]; apply: leq_trans n8. Qed.
imports: Coq(BinNat) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div)