proposition: Theorem wmult_assoc : forall sz (x y z : word sz), x ^* (y ^* z) = x ^* y ^* z.
proof: Proof. intros sz x y z; repeat rewrite wmult_alt; unfold wmultN, wordBinN; intros. repeat match goal with | [ |- context[wordToNat (natToWord ?sz ?w)] ] => let Heq := fresh "Heq" in destruct (wordToNat_natToWord sz w) as [? [Heq ?]]; rewrite Heq end. rewrite Nat.mul_sub_distr_r. rewrite Nat.mul_sub_distr_l. match goal with | [ |- natToWord _ (_ - _ * (?x0' * _)) = natToWord _ (_ - ?x1' * _ * _) ] => rename x0' into x0, x1' into x1 end. rewrite (Nat.mul_assoc (wordToNat x) x0). rewrite <- (Nat.mul_assoc x1). rewrite (Nat.mul_comm (pow2 sz)). rewrite (Nat.mul_assoc x1). repeat rewrite drop_sub; auto with arith. rewrite (Nat.mul_comm x1). rewrite <- (Nat.mul_assoc (wordToNat x)). rewrite (Nat.mul_comm (wordToNat y)). rewrite Nat.mul_assoc. rewrite (Nat.mul_comm (wordToNat x)). repeat rewrite <- Nat.mul_assoc. auto with arith. repeat rewrite <- Nat.mul_assoc. auto with arith. 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