proposition: Lemma nds_sol_v n: nat_to_B (Nds.nds_sol n) = nds_sol(nat_to_B n).
proof: Proof. case:n => [ | n]; first by rewrite/nds_sol /= succ_zero; Ytac0. rewrite (nds_sol_nz (nat_to_B_Nat n)). rewrite /Nds.nds_sol /Nds.nds_value/nds_sol' /nds_explicit. have <-: nat_to_B 7 = \7c by rewrite /card_seven - nat_to_B6. rewrite nat_to_B_ifle; Ytac h; Ytac0; clear h; first by apply: ndsC_v. set u4 := Nds.ndsC 4. set u5 := Nds.ndsC 5. set u6 := Nds.ndsC 6. have ->: ndsC \5c = nat_to_B u5 by rewrite ndsC_v nat_to_B5. have ->: ndsC \6c = nat_to_B u6 by rewrite ndsC_v nat_to_B6. have ->: ndsC \4c = nat_to_B u4 by rewrite ndsC_v nat_to_B4. have NB2:=nat_to_B2. have NB3: nat_to_B 3 = \3c by rewrite /= succ_zero succ_one . rewrite -nat_to_B5 - NB3 - NB2 - nat_to_B1; clear NB3 NB2. move: (nat_to_B_quorem n 5) => [<- <-]. rewrite !nat_to_B_ifeq. pose nbp := nat_to_B_pow; pose nbm:= nat_to_B_prod. Ytac eq0; Ytac0; first by rewrite nbp. Ytac eq1; Ytac0; first by rewrite -nat_to_B_diff subn1 nbm nbp. Ytac eq2; Ytac0; first by rewrite nbm nbp nbp - subn2 -nat_to_B_diff. Ytac eq3; Ytac0; last by rewrite nbm nbp. Ytac eq4; Ytac0; first by rewrite nbp. by Ytac eq5;Ytac0; rewrite nbm ! nbp -? nat_to_B_diff. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)