src/HOL/GCD.thy
changeset 54489 03ff4d1e6784
parent 54437 0060957404c7
child 54867 c21a2465cac1
     1.1 --- a/src/HOL/GCD.thy	Tue Nov 19 01:30:14 2013 +0100
     1.2 +++ b/src/HOL/GCD.thy	Tue Nov 19 10:05:53 2013 +0100
     1.3 @@ -134,6 +134,14 @@
     1.4  lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
     1.5    by (simp add: gcd_int_def)
     1.6  
     1.7 +lemma gcd_neg_numeral_1_int [simp]:
     1.8 +  "gcd (- numeral n :: int) x = gcd (numeral n) x"
     1.9 +  by (fact gcd_neg1_int)
    1.10 +
    1.11 +lemma gcd_neg_numeral_2_int [simp]:
    1.12 +  "gcd x (- numeral n :: int) = gcd x (numeral n)"
    1.13 +  by (fact gcd_neg2_int)
    1.14 +
    1.15  lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
    1.16  by(simp add: gcd_int_def)
    1.17