proposition: Lemma nds_sol_Bourbaki_conc (f := nds_sol): forall n, natp n -> card_15 <=c n -> f(n +c \5c) = (ndsC \5c) *c f n.
proof: Proof. move => n nN. move:(B_to_nat_pa nN); set N := (B_to_nat n) => nv. rewrite - nv - nat_to_B5 - nat_to_B_sum /f - nds_sol_v - nds_sol_v. move/nat_to_B_le/ Nds.nds_sol_rec5 => ->. by rewrite - ndsC_v nat_to_B_prod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)