proposition: Lemma wmod_plus_distr: forall sz (a b m: word sz), (exists k, (wordToN m * k)%N = Npow2 sz) -> (a ^+ b) ^% m = ((a ^% m) ^+ (b ^% m)) ^% m.
proof: Proof. intros. destruct H as [k E]. assert (wordToN m <> 0%N) as H. { intro C. rewrite C in E. simpl in E. symmetry in E. apply Npow2_not_zero in E. assumption. } unfold wplus, wmod, wordBin. pose proof (wordToN_bound a). remember (wordToN a) as c. clear Heqc a. pose proof (wordToN_bound b). remember (wordToN b) as d. clear Heqd b. pose proof (wordToN_bound m). remember (wordToN m) as n. clear Heqn m. pose proof (N.mod_upper_bound c n H). pose proof (N.mod_upper_bound d n H). rewrite (@wordToN_NToWord_2 sz (c mod n)) by nomega. rewrite (@wordToN_NToWord_2 sz (d mod n)) by nomega. repeat match goal with | |- context [wordToN (NToWord ?sz ?n)] => let k := fresh "k" in let E := fresh "E" in let B := fresh "B" in destruct (wordToN_NToWord sz n) as [ k [E B] ]; rewrite E in *; clear E end. rewrite <- E in *. rewrite <- Nminus_mod_idemp_r by assumption. rewrite <- (@Nminus_mod_idemp_r (c mod n + d mod n)) by assumption. rewrite (N.mul_comm n k). do 2 rewrite N.mul_assoc. do 2 rewrite N.mod_mul by assumption. do 2 rewrite N.sub_0_r. f_equal. apply N.add_mod. assumption. 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