proposition: Corollary toZp_addB n (p1 p2: BITS n.+1) : toZp (addB p1 p2) = (toZp p1 + toZp p2)%R.
proof: Proof. apply val_inj. rewrite /toZp. rewrite toNat_addB. rewrite /= Zp_cast; last apply pow2_gt1. rewrite (@modn_small (toNat p1)); last apply toNatBounded. rewrite (@modn_small (toNat p2)); last apply toNatBounded. by rewrite 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)