src/HOL/Number_Theory/Cong.thy
changeset 66817 0b12755ccbb2
parent 66453 cc19f7ca2ed6
child 66837 6ba663ff2b1c
     1.1 --- a/src/HOL/Number_Theory/Cong.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Number_Theory/Cong.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -86,8 +86,7 @@
     1.4    "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> m \<ge> 0 \<Longrightarrow> [nat x = nat y] (mod (nat m)) \<longleftrightarrow> [x = y] (mod m)"
     1.5    for x y m :: int
     1.6    unfolding cong_int_def cong_nat_def
     1.7 -  by (metis Divides.transfer_int_nat_functions(2) nat_0_le nat_mod_distrib)
     1.8 -
     1.9 +  by (metis int_nat_eq nat_mod_distrib zmod_int)
    1.10  
    1.11  declare transfer_morphism_nat_int [transfer add return: transfer_nat_int_cong]
    1.12