proposition: Lemma ZToWord_Npow2_sub: forall sz z, ZToWord sz (z - Z.of_N (Npow2 sz)) = ZToWord sz z.
proof: Proof. unfold ZToWord; intros. remember (z - Z.of_N (Npow2 sz))%Z as zz. destruct z. - destruct zz. + assert (Z.of_N (Npow2 sz) = 0)%Z by lia. change 0%Z with (Z.of_N 0%N) in H. apply N2Z.inj in H. exfalso; eapply Npow2_not_zero; eauto. + pose proof (N2Z.is_nonneg (Npow2 sz)). destruct (Z.of_N (Npow2 sz)); simpl in Heqzz, H; try discriminate. pose proof (Pos2Z.neg_is_neg p0); lia. + assert (Z.of_N (Npow2 sz) = Z.pos p). { rewrite Z.sub_0_l, <-Pos2Z.opp_pos in Heqzz. apply Z.opp_inj in Heqzz; auto. } rewrite <-N2Z.inj_pos in H. apply N2Z.inj in H. rewrite posToWord_nat, <-positive_N_nat, <-H. rewrite Npow2_nat, natToWord_pow2. rewrite wzero_wneg. apply eq_sym, wzero'_def. - destruct zz. + assert (Z.of_N (Npow2 sz) = Z.pos p) by lia. rewrite <-N2Z.inj_pos in H. apply N2Z.inj in H. rewrite posToWord_nat, <-positive_N_nat, <-H. rewrite Npow2_nat, natToWord_pow2. apply wzero'_def. + assert (Z.pos p = Z.pos p0 + Z.of_N (Npow2 sz))%Z by lia. do 2 rewrite <-N2Z.inj_pos in H. rewrite <-N2Z.inj_add in H. apply N2Z.inj in H. apply eq_sym. do 2 rewrite posToWord_nat, <-positive_N_nat. rewrite H, N2Nat.inj_add, Npow2_nat. apply natToWord_pow2_add. + assert (Z.pos p - Z.neg p0 = Z.of_N (Npow2 sz))%Z by lia. simpl in H. remember (Npow2 sz) as n; destruct n; [exfalso; eapply Npow2_not_zero; eauto|]. rewrite N2Z.inj_pos in H; inversion H; subst; clear H. apply eq_sym, sub_0_eq. rewrite wminus_def, wneg_idempotent. apply Npos_Npow2_wzero; auto. - destruct zz. + assert (Z.neg p = Z.of_N (Npow2 sz))%Z by lia. pose proof (N2Z.is_nonneg (Npow2 sz)). rewrite <-H in H0. pose proof (Pos2Z.neg_is_neg p); lia. + assert (Z.neg p = Z.pos p0 + Z.of_N (Npow2 sz))%Z by lia. pose proof (N2Z.is_nonneg (Npow2 sz)). destruct (Z.of_N (Npow2 sz)); simpl in H; try discriminate. pose proof (Pos2Z.neg_is_neg p1); lia. + assert (Pos.to_nat p0 = Pos.to_nat p + pow2 sz). { rewrite <-Npow2_nat. do 2 rewrite <-positive_N_nat. rewrite <-N2Nat.inj_add. f_equal. pose proof (N2Z.is_nonneg (Npow2 sz)). remember (Z.of_N (Npow2 sz)) as z; destruct z. { change 0%Z with (Z.of_N 0) in Heqz. apply N2Z.inj in Heqz. exfalso; eapply Npow2_not_zero; eauto. } { simpl in Heqzz; inversion Heqzz; subst. rewrite <-N2Z.inj_pos in Heqz. apply N2Z.inj in Heqz. rewrite <-Heqz. reflexivity. } { pose proof (Zlt_neg_0 p1); lia. } } f_equal. do 2 rewrite posToWord_nat. rewrite H. apply natToWord_pow2_add. 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