[STATEMENT]
lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd m (k * m + n) = gcd m n
[PROOF STEP]
by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)