proposition: Corollary inZp_addBn n (p:BITS n.+1) m : toZp (p +# m) = inZp (toNat p + m).
proof: Proof. apply val_inj. rewrite /inZp/toZp. rewrite toNat_addBn. rewrite /= Zp_cast; last apply pow2_gt1. apply modn_mod. 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)