proposition: Lemma toNatMod_decB n (p: BITS n) : toNat (decB p) = (toNat p + (2^n).-1) %[mod 2^n].
proof: Proof. rewrite toNat_decB. case E: (p == #0) => //. + rewrite (eqP E) {E}. by rewrite toNat_fromNat0 add0n. + apply negbT in E. destruct (nonZeroIsSucc E) as [m E']. rewrite E'. rewrite succnK. rewrite -!subn1. rewrite addnBA. rewrite addnC. rewrite -addnBA => //. rewrite subn1 succnK. by rewrite modnDl. apply expn_gt0. 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