proposition: Lemma wminus_wminusZ: forall (sz : nat) (w1 w2 : word sz), w1 ^- w2 = wminusZ w1 w2.
proof: Proof. unfold wminusZ, wminus, wordBinZ. intros. rewrite <- Z.add_opp_r. rewrite wplus_wplusZ. unfold wplusZ, wordBinZ. destruct sz. - do 2 rewrite ZToWord_sz0. reflexivity. - destruct (weq w2 (wpow2 sz)). + subst. rewrite wpow2_wneg. replace (wordToZ w1 + - wordToZ (wpow2 sz))%Z with (wordToZ w1 + wordToZ (wpow2 sz) - 2 * wordToZ (wpow2 sz))%Z by lia. replace (2 * wordToZ (wpow2 sz))%Z with (- 1 * Z.of_N (Npow2 (S sz)))%Z. * symmetry. apply ZToWord_Npow2_sub_z. * rewrite wordToZ_wordToN. rewrite wpow2_wmsb. rewrite wpow2_Npow2. rewrite Npow2_S. rewrite N2Z.inj_add. lia. + rewrite wneg_wordToZ by assumption. reflexivity. 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