proposition: Lemma nds_sol_nz n: natp n -> nds_sol (csucc n) = nds_sol' n.
proof: Proof. by move => nN; rewrite /nds_sol (Y_false (@succ_nz _)) (cpred_pr1 (CS_nat nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)