proposition: Lemma wneg_WS_1: forall sz (w: word sz), wneg w~1 = (wnot w)~1.
proof: Proof. intros. apply wordToN_inj. simpl; rewrite wnot_def. unfold wneg. rewrite wordToN_NToWord_2 by (apply N.sub_lt; [apply N.lt_le_incl, wordToN_bound|nomega]). rewrite wordToN_NToWord_2. - rewrite wordToN_WS_1. change (Npow2 (S sz)) with (2 * Npow2 sz)%N. rewrite N.sub_add_distr. rewrite <-N.mul_sub_distr_l. assert (Npow2 sz - wordToN w <> 0)%N by (pose proof (wordToN_bound w); nomega). remember (Npow2 sz - wordToN w)%N as n; clear Heqn. destruct n; [intuition idtac|]. remember (N.pos p - 1)%N as pp; destruct pp. + apply eq_sym, N.sub_0_le in Heqpp. apply N.le_1_r in Heqpp; destruct Heqpp; [discriminate|]. rewrite H0; reflexivity. + change (N.pos p0~0) with (2 * N.pos p0)%N. rewrite Heqpp. rewrite <-N.add_1_r. rewrite N.mul_sub_distr_l. clear; destruct p; cbn; reflexivity. - rewrite <-N.sub_add_distr. apply N.sub_lt; [|nomega]. pose proof (wordToN_bound w). apply N.le_succ_l in H. rewrite N.add_1_r; 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