proposition: Lemma extz_is_mult_pow2_neg: forall sz n d, extz (wneg (natToWord sz n)) d = wneg (natToWord (d + sz) (pow2 d * n)).
proof: Proof. intros. induction d. - unfold extz. rewrite combine_0_n. simpl. f_equal. f_equal. lia. - unfold extz in *. change (pow2 (S d) * n) with (2 * pow2 d * n). rewrite <- Nat.mul_assoc. change ((S d) + sz) with (S (d + sz)) in *. rewrite <- natToWord_times2. simpl. fold natToWord. f_equal. rewrite wneg_WS_0. f_equal. exact IHd. 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