proposition: Lemma toZp_invB n (p:BITS n.+1) : toZp (invB p) = (-toZp p - 1)%R.
proof: Proof. apply val_inj. rewrite /= Zp_cast; last apply pow2_gt1. rewrite toNat_invB. rewrite (@modn_small 1); last apply pow2_gt1. rewrite (@modn_small (toNat p)); last apply toNatBounded. rewrite (@modn_small (2^n.+1-1)); last apply pow2_sub_ltn. rewrite modn_small. case E: (toNat p) => [| p']. + rewrite 2!subn0. rewrite modnn add0n. rewrite modn_small; last apply pow2_sub_ltn. by rewrite subn1. rewrite -subn1 -subnDA add1n. rewrite (@modn_small (2^n.+1 - p'.+1)); last apply pow2_sub_ltn. rewrite addnBA; last apply expn_gt0. rewrite addnC. rewrite -addnBA. rewrite addnC. rewrite modnDr. rewrite -subnDA. rewrite addn1. rewrite modn_small; last apply pow2_sub_ltn. done. have B:= toNatBounded p. rewrite -E. by rewrite subn_gt0. rewrite -subn1. rewrite -subnDA. rewrite add1n. apply pow2_sub_ltn. 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)