tests/PGCD/PGCD_PGCD_common_div_a_b_1.thy

   1 theory PGCD_PGCD_common_div_a_b_1
   2 imports Why3
   3 begin
   4
   5 why3_open "PGCD_PGCD_common_div_a_b_1.xml"
   6
   7 why3_vc common_div_a_b
   8 proof -
   9   from assms have "\<exists>pa pb::int. (a-b) = pa * k \<and> b = pb * k" using common_div_def and divides_def by simp
  10   then obtain pa pb where "(a-b) = pa * k" and "b = pb * k" by auto
  11   hence "a-b+b = pa * k + pb * k" by simp
  12   hence "a = (pa + pb) * k" using Mul_distr_r by simp
  13   hence "divides k a" using divides_def by simp
  14   thus "common_div a b k" using assms and common_div_def by simp
  15 qed
  16
  17 why3_end
  18
  19 end