proposition: Lemma natToWord_mult : forall sz n m, natToWord sz (n * m) = natToWord _ n ^* natToWord _ m.
proof: Proof. destruct sz; intuition. rewrite wmult_alt. unfold wmultN, wordBinN. destruct (wordToNat_natToWord (S sz) n); intuition. destruct (wordToNat_natToWord (S sz) m); intuition. rewrite H0; rewrite H2; clear H0 H2. replace ((n - x * pow2 (S sz)) * (m - x0 * pow2 (S sz))) with ((n - x * pow2 (S sz)) * m - (n - x * pow2 (S sz)) * (x0 * pow2 (S sz))) by (rewrite Nat.mul_sub_distr_l; auto). rewrite Nat.mul_assoc; rewrite drop_sub. repeat rewrite Nat.mul_comm with (m:=m). replace (m * (n - x * pow2 (S sz))) with (m * n - m * (x * pow2 (S sz))) by (rewrite Nat.mul_sub_distr_l; auto). rewrite Nat.mul_assoc; rewrite drop_sub. auto. rewrite <- Nat.mul_assoc; apply Nat.mul_le_mono_l; auto. rewrite <- Nat.mul_assoc; apply Nat.mul_le_mono_l; auto. 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