# HG changeset patch
# User nipkow
# Date 1245455619 -7200
# Node ID b9299916d618f07cc50e01a913938edad4afba16
# Parent  60317e5211a2602050ca38b4b35498ef512baa6d
new lemmas and tuning

diff -r 60317e5211a2 -r b9299916d618 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Fri Jun 19 22:49:38 2009 +0200
+++ b/src/HOL/GCD.thy	Sat Jun 20 01:53:39 2009 +0200
@@ -1421,6 +1421,18 @@
 lemma int_lcm_dvd2 [iff]: "(n::int) dvd lcm m n"
   by (subst int_lcm_commute, rule int_lcm_dvd1)
 
+lemma dvd_lcm_if_dvd1_nat: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
+by(metis nat_lcm_dvd1 dvd_trans)
+
+lemma dvd_lcm_if_dvd2_nat: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
+by(metis nat_lcm_dvd2 dvd_trans)
+
+lemma dvd_lcm_if_dvd1_int: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
+by(metis int_lcm_dvd1 dvd_trans)
+
+lemma dvd_lcm_if_dvd2_int: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
+by(metis int_lcm_dvd2 dvd_trans)
+
 lemma nat_lcm_unique: "(a::nat) dvd d \<and> b dvd d \<and>
     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   by (auto intro: dvd_anti_sym nat_lcm_least)