proposition: Lemma wnot_def: forall sz (w: word sz), wnot w = NToWord sz (Npow2 sz - wordToN w - 1).
proof: Proof. dependent induction w; cbn; [reflexivity|]. destruct b; cbn. - rewrite IHw; clear IHw. rewrite <-NToWord_WS_0. f_equal. destruct (Npow2 n); [reflexivity|]. destruct (wordToN w). + change (N.pos p~0) with (2 * N.pos p)%N. do 2 rewrite N.mul_sub_distr_l. do 2 rewrite <-N.sub_add_distr. reflexivity. + change (N.pos p~0) with (2 * N.pos p)%N. change (N.pos p0~0) with (2 * N.pos p0)%N. rewrite <-N.add_1_l. do 2 rewrite N.mul_sub_distr_l. do 2 rewrite <-N.sub_add_distr. rewrite N.add_comm with (n:= 1%N). rewrite <-N.add_assoc. reflexivity. - rewrite IHw; clear IHw. rewrite <-NToWord_WS_1. f_equal. pose proof (wordToN_bound w). remember (Npow2 n) as pn; destruct pn; [exfalso; eapply Npow2_not_zero; eauto|clear Heqpn]. destruct (wordToN w). + change (N.pos p~0) with (2 * N.pos p)%N. do 2 rewrite N.mul_sub_distr_l. do 2 rewrite <-N.sub_add_distr. destruct p; cbn; reflexivity. + change (N.pos p~0) with (2 * N.pos p)%N. change (N.pos p0~0) with (2 * N.pos p0)%N. rewrite N.mul_sub_distr_l. rewrite <-N.mul_sub_distr_l with (n:= N.pos p). assert (exists pp, N.pos p - N.pos p0 = N.pos pp)%N. { apply N.sub_gt in H. destruct (N.pos p - N.pos p0)%N; [intuition idtac|]. eexists; reflexivity. } destruct H0; rewrite H0. destruct x; cbn; 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