proposition: Lemma toZp_incB n (p:BITS n.+1) : toZp (incB p) = (toZp p + 1)%R.
proof: Proof. apply val_inj. rewrite /= Zp_cast; last apply pow2_gt1. rewrite modnDml modnDmr addn1 toNat_incB. case E: (p == ones _) => //. by rewrite (eqP E) toNat_ones_succ modnn mod0n. 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)