equal
deleted
inserted
replaced
800 let ?c = "zgcd a b" |
800 let ?c = "zgcd a b" |
801 case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto |
801 case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto |
802 then have "?c \<noteq> 0" by simp |
802 then have "?c \<noteq> 0" by simp |
803 then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat) |
803 then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat) |
804 moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b" |
804 moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b" |
805 by (simp add: times_div_mod_plus_zero_one.mod_div_equality) |
805 by (simp add: semiring_div_class.mod_div_equality) |
806 moreover have "a mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric]) |
806 moreover have "a mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric]) |
807 moreover have "b mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric]) |
807 moreover have "b mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric]) |
808 ultimately show ?thesis |
808 ultimately show ?thesis |
809 by (simp add: mult_rat [symmetric]) |
809 by (simp add: mult_rat [symmetric]) |
810 qed |
810 qed |