equal
deleted
inserted
replaced
131 lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y" |
131 lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y" |
132 by (simp add: gcd_int_def) |
132 by (simp add: gcd_int_def) |
133 |
133 |
134 lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y" |
134 lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y" |
135 by (simp add: gcd_int_def) |
135 by (simp add: gcd_int_def) |
|
136 |
|
137 lemma gcd_neg_numeral_1_int [simp]: |
|
138 "gcd (- numeral n :: int) x = gcd (numeral n) x" |
|
139 by (fact gcd_neg1_int) |
|
140 |
|
141 lemma gcd_neg_numeral_2_int [simp]: |
|
142 "gcd x (- numeral n :: int) = gcd x (numeral n)" |
|
143 by (fact gcd_neg2_int) |
136 |
144 |
137 lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y" |
145 lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y" |
138 by(simp add: gcd_int_def) |
146 by(simp add: gcd_int_def) |
139 |
147 |
140 lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)" |
148 lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)" |