proposition: Lemma ndsC_v n: nat_to_B (Nds.ndsC n) = ndsC (nat_to_B n).
proof: Proof. rewrite Nds.ndsCE /ndsC; case:n; first by rewrite cprod0l. move => n /=; rewrite (cpred_pr2 (nat_to_B_Nat n)). by rewrite nat_to_B_prod nat_to_B_pow /= succ_zero succ_one. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)