src/HOL/Divides.ML

 by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
 by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2);
 by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
 qed "dvd_mod_imp_dvd";
 
+Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd (m mod n)";
+by (div_undefined_case_tac "n=0" 1);
+by (Clarify_tac 1);
+by (Full_simp_tac 1);
+by (rename_tac "j" 1);
+by (res_inst_tac 
+    [("x", "(((k div j)*j + k mod j) - ((f*k) div (f*j)) * j)")] 
+    exI 1);
+by (asm_simp_tac
+    (simpset() addsimps [diff_mult_distrib2, mod_mult_distrib2 RS sym, 
+			 add_mult_distrib2]) 1);
+qed "dvd_mod";
+
+Goal "k dvd n ==> (k::nat) dvd (m mod n) = k dvd m";
+by (blast_tac (claset() addIs [dvd_mod_imp_dvd, dvd_mod]) 1); 
+qed "dvd_mod_iff";
+
 Goalw [dvd_def]  "!!k::nat. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
 by (etac exE 1);
 by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
 qed "dvd_mult_cancel";