equal
deleted
inserted
replaced
90 |
90 |
91 lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n" |
91 lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n" |
92 proof - |
92 proof - |
93 assume "0 < n" |
93 assume "0 < n" |
94 then have "gcd (n * k + m) n = gcd n (m mod n)" |
94 then have "gcd (n * k + m) n = gcd n (m mod n)" |
95 by (simp add: gcd_non_0_nat add_commute) |
95 by (simp add: gcd_non_0_nat add.commute) |
96 also from `0 < n` have "\<dots> = gcd m n" |
96 also from `0 < n` have "\<dots> = gcd m n" |
97 by (simp add: gcd_non_0_nat) |
97 by (simp add: gcd_non_0_nat) |
98 finally show ?thesis . |
98 finally show ?thesis . |
99 qed |
99 qed |
100 |
100 |