proposition: Lemma wmod_divides: forall sz (a b: word sz), a ^% b = $0 -> exists k, a = b ^* k.
proof: Proof. intros. destruct (weq b $0). - subst b. rewrite wmod_0_r in *. subst a. exists (natToWord sz 0). symmetry. apply wmult_neut_r. - unfold wmod, wmult, wordBin in *. pose proof (N.mod_divides (wordToN a) (wordToN b)) as P. apply wordToN_neq_0 in n. specialize (P n). destruct P as [ [k P] _]. + apply (f_equal (@wordToN sz)) in H. rewrite wordToN_NToWord_2 in H. * rewrite H. apply wordToN_0. * 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 (N.mod_upper_bound c d n). nomega. + exists (NToWord sz (k - k / (Npow2 sz) * Npow2 sz)). rewrite wordToN_NToWord_2. { rewrite N.mul_sub_distr_l. rewrite N.mul_assoc. rewrite drop_sub_N. - rewrite <- P. symmetry. apply NToWord_wordToN. - rewrite <- N.mul_assoc. rewrite <- (N.mul_comm (Npow2 sz)). apply N.mul_le_mono_l. apply (N.mul_div_le k (Npow2 sz)). apply Npow2_not_zero. } { rewrite <- N.mul_comm. rewrite <- N.mod_eq by (apply Npow2_not_zero). apply N.mod_upper_bound. apply Npow2_not_zero. } 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