proposition: Lemma nds_sol_max n: 1 < n -> exists2 k, 0 < k < n & (nds_sol n = (ndsC k) * (nds_sol (n - k))).
proof: Proof. move=> np. move: (nds_k_of_bd np) (nds_sol_with_k np) => ha hb. by exists (nds_k_of n). Qed.
imports: Coq(BinNat) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div)