proposition: Theorem wmult_plus_distr : forall sz (x y z : word sz), (x ^+ y) ^* z = (x ^* z) ^+ (y ^* z).
proof: Proof. intros sz x y z; repeat rewrite wmult_alt; repeat rewrite wplus_alt; unfold wmultN, wplusN, 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. match goal with | [ |- natToWord _ (_ - ?x0' * _ * _) = natToWord _ (_ - ?x1' * _ + (_ - ?x2' * _)) ] => rename x0' into x0, x1' into x1, x2' into x2 end. rewrite <- (Nat.mul_assoc x0). rewrite (Nat.mul_comm (pow2 sz)). rewrite (Nat.mul_assoc x0). replace (wordToNat x * wordToNat z - x1 * pow2 sz + (wordToNat y * wordToNat z - x2 * pow2 sz)) with (wordToNat x * wordToNat z + wordToNat y * wordToNat z - x1 * pow2 sz - x2 * pow2 sz). repeat rewrite drop_sub; auto with arith. all: try rewrite (Nat.mul_comm x0); try rewrite (Nat.mul_comm (wordToNat x + wordToNat y)); try rewrite <- (Nat.mul_assoc (wordToNat z)); auto with arith; generalize dependent (wordToNat x * wordToNat z); generalize dependent (wordToNat y * wordToNat z); intros; lia. 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