proposition: Lemma wordToZ_WS_1: forall sz (w: word (S sz)), wordToZ w~1 = (2 * wordToZ w + 1)%Z.
proof: Proof. intros. destruct (destruct_word_S w) as [v [b E]]. rewrite E. clear w E. rename v into w. unfold wordToZ. rewrite wmsb_ws. remember (wmsb (WS b w) false) as msb. destruct msb. - rewrite wneg_WS_1. rewrite wordToN_WS_1. rewrite wnot_def. unfold wneg. assert (Npow2 (S sz) - wordToN (WS b w) <> 0)%N. { pose proof (wordToN_bound (WS b w)); nomega. } assert (Npow2 (S sz) - wordToN (WS b w) < Npow2 (S sz))%N. { apply N.sub_lt. { apply N.lt_le_incl, wordToN_bound. } { assert (wordToN (WS b w) <> 0)%N. { replace 0%N with (wordToN (wzero (S sz))). { intro Hx. apply wordToN_inj in Hx. rewrite Hx in Heqmsb. rewrite wmsb_wzero in Heqmsb; discriminate. } { rewrite wordToN_nat. unfold wzero; rewrite roundTrip_0; reflexivity. } } nomega. } } remember (Npow2 (S sz) - wordToN (WS b w))%N as n; clear Heqn. rewrite wordToN_NToWord_2 by nomega. rewrite wordToN_NToWord_2 by nomega. destruct n; [intuition idtac|]. destruct p; cbn; reflexivity. - rewrite wordToN_WS_1. destruct (wordToN (WS b w)); cbn; lia. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Classes.Equivalence Coq.Arith.PeanoNat Coq.ZArith.BinInt  Coq.Arith.Arith Coq.NArith.NArith Coq.Bool.Bool Coq.ZArith.ZArith Coq.Logic.Eqdep_dec Coq.Logic.EqdepFacts Coq.Program.Tactics Coq.Program.Equality Coq.setoid_ring.Ring Coq.setoid_ring.Ring_polynom bbv.Nomega bbv.ZLib bbv.NatLib bbv.NLib bbv.N_Z_nat_conversions bbv.DepEq bbv.DepEqNat bbv.ReservedNotations Coq.micromega.Lia