proposition: Lemma nds_k_of_bd n: natp n -> \1c <c n -> \0c <c nds_k_of n /\ nds_k_of n <c n.
proof: Proof. move => nN np. move: (B_to_nat_pa nN); set p := (B_to_nat n) => eqa. have p1: 1 < p by apply/nat_to_B_gt1; rewrite eqa. move: (Nds.nds_k_of_bd p1) => /andP [/nat_to_B_pos ha /nat_to_B_lt]. by move: ha; rewrite nds_k_of_v eqa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)