proposition: Lemma toZp_negB n (p:BITS n.+1) : toZp (negB p) = (-toZp p)%R.
proof: Proof. apply val_inj. rewrite /= Zp_cast; last apply pow2_gt1. rewrite toNat_negB. case E: (toNat p) => [| n']. + simpl. rewrite modn_small. by rewrite subn0 modnn. apply expn_gt0. + simpl. rewrite modn_small. rewrite (@modn_small (n'.+1)). rewrite modn_small. done. apply pow2_sub_ltn. rewrite -E. apply toNatBounded. 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)