src/HOL/Divides.thy
changeset 14437 92f6aa05b7bb
parent 14430 5cb24165a2e1
child 14640 b31870c50c68
equal deleted inserted replaced
14436:77017c49c004 14437:92f6aa05b7bb
   477 apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
   477 apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
   478 (* case n \<le> Suc(na) *)
   478 (* case n \<le> Suc(na) *)
   479 apply (simp add: not_less_iff_le le_Suc_eq mod_geq)
   479 apply (simp add: not_less_iff_le le_Suc_eq mod_geq)
   480 apply (auto simp add: Suc_diff_le diff_less le_mod_geq)
   480 apply (auto simp add: Suc_diff_le diff_less le_mod_geq)
   481 done
   481 done
       
   482 
       
   483 lemma nat_mod_div_trivial [simp]: "m mod n div n = (0 :: nat)"
       
   484 by (case_tac "n=0", auto)
       
   485 
       
   486 lemma nat_mod_mod_trivial [simp]: "m mod n mod n = (m mod n :: nat)"
       
   487 by (case_tac "n=0", auto)
   482 
   488 
   483 
   489 
   484 subsection{*The Divides Relation*}
   490 subsection{*The Divides Relation*}
   485 
   491 
   486 lemma dvdI [intro?]: "n = m * k ==> m dvd n"
   492 lemma dvdI [intro?]: "n = m * k ==> m dvd n"