proposition: Lemma toZp_decB n (p:BITS n.+1) : toZp (decB p) = (toZp p - 1)%R.
proof: Proof. apply val_inj. set N := n.+1. set D :=decB p. rewrite /= Zp_cast; last apply pow2_gt1. rewrite /D {D}. rewrite toNatMod_decB. replace (1 %% 2^N) with 1. rewrite (@modn_small (2^N - 1)). rewrite (@modn_small (toNat p)). by rewrite subn1. apply toNatBounded. apply pow2_sub_ltn. rewrite modn_small => //; last apply pow2_gt1. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations mathcomp(ssralg)