proposition: Lemma toZp_subB n (p q: BITS n.+1) : toZp (subB p q) = (toZp p - toZp q)%R.
proof: Proof. rewrite subB_is_dropmsb_adcB_invB. apply val_inj. rewrite toZp_dropmsb /toZpAux. rewrite toNat_adcBmain toNat_invB. rewrite add1n. rewrite /inZp/= Zp_cast; last apply pow2_gt1. rewrite (@modn_small (toNat p)); last apply toNatBounded. rewrite (@modn_small (toNat q)); last apply toNatBounded. rewrite -addn1. rewrite -subn1. rewrite -subnDA. rewrite addnAC. rewrite -addnA. rewrite addn1 add1n. rewrite -subSn; last apply toNatBounded. case E: (toNat q) => [| n']. rewrite !subn0 modnn addn0. rewrite subn1. rewrite succnK. by rewrite modnDr. rewrite (@modn_small (2^n.+1 - n'.+1)); last apply pow2_sub_ltn. done. 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)