proposition: Lemma wordToZ_size': forall sz (w: word (S sz)), (- Z.of_nat (pow2 sz) <= wordToZ w < Z.of_nat (pow2 sz))%Z.
proof: Proof. unfold wordToZ; intros. remember (wmsb w false) as msb; destruct msb. - destruct (weq w (wpow2 _)). + subst; rewrite wpow2_wneg. rewrite wpow2_Npow2. remember (Npow2 sz) as np. destruct np; [exfalso; eapply Npow2_not_zero; eauto|]. split. * rewrite <-Pos2Z.opp_pos, <-N2Z.inj_pos. rewrite Heqnp. rewrite <-Npow2_nat. rewrite N_nat_Z. reflexivity. * etransitivity. { apply Pos2Z.neg_is_neg. } { change 0%Z with (Z.of_nat 0). apply Nat2Z.inj_lt. apply zero_lt_pow2. } + assert (wordToN (wneg w) < Npow2 sz)%N. { apply wmsb_false_bound. eapply wmsb_wneg_true; eauto. } remember (wordToN (wneg w)) as ww; clear Heqww. destruct ww; simpl. * split; try lia; change 0%Z with (Z.of_nat 0); apply Nat2Z.inj_lt; apply zero_lt_pow2. * split. { rewrite <-Pos2Z.opp_pos, <-N2Z.inj_pos. rewrite <-Npow2_nat. rewrite N_nat_Z. rewrite <-Z.opp_le_mono. apply N2Z.inj_le. apply N.lt_le_incl. assumption. } { etransitivity. { apply Pos2Z.neg_is_neg. } { change 0%Z with (Z.of_nat 0). apply Nat2Z.inj_lt. apply zero_lt_pow2. } } - apply eq_sym, wmsb_false_bound in Heqmsb. destruct (wordToN w); simpl. * split; try lia; change 0%Z with (Z.of_nat 0); apply Nat2Z.inj_lt; apply zero_lt_pow2. * split. { etransitivity. { apply Z.opp_nonpos_nonneg. change 0%Z with (Z.of_nat 0). apply Nat2Z.inj_le. pose proof (zero_lt_pow2 sz); lia. } { pose proof (Pos2Z.is_pos p); lia. } } { rewrite <-N2Z.inj_pos. rewrite <-Npow2_nat. rewrite N_nat_Z. apply N2Z.inj_lt. assumption. } 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