proposition: Lemma nds_sol_rec5 n: 15 <= n -> nds_sol (n + 5) = ndsC 5 * nds_sol n.
proof: Proof. move => ha. have lt1: 1 < n +5 by rewrite addnC. by rewrite (nds_sol_with_k lt1) addnC -(subnKC ha) addnA. Qed.
imports: Coq(BinNat) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div)