试图证明一个类型是`euclidean_semiring`的实例(在Isabelle中)

instance my_type :: euclidean_semiring
proof
  fix a b c :: my_type
  show "a + (b + c) = (a + b) + c" by simp
  show "a * (b * c) = (a * b) * c" by simp
  show "a + b = b + a" by simp
  show "a * b = b * a" by simp
  show "0 + a = a" by simp
  show "a + 0 = a" by simp
  show "1 * a = a" by simp
  show "a * 1 = a" by simp
  show "a * (b + c) = a * b + a * c" by simp
  show "a * (b + c) = a * b + a * c" by simp
  show "a * (b + c) = a * b + a * c" by simp
  show "a * (b + c) = a * b + a * c" by simp
  show "a div b * b + a mod b = a" by simp
  show "a div b * b + a mod b = a" by simp
qed