src/HOL/Presburger.thy
changeset 68157 057d5b4ce47e
parent 68103 b2d84b1114fa
child 69605 3dda49e08b9d
     1.1 --- a/src/HOL/Presburger.thy	Sat May 12 17:53:12 2018 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Sat May 12 22:20:46 2018 +0200
     1.3 @@ -495,11 +495,11 @@
     1.4    by presburger
     1.5  
     1.6  lemma odd_mod_4_div_2:
     1.7 -  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
     1.8 +  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - Suc 0) div 2)"
     1.9    by presburger
    1.10  
    1.11  lemma even_mod_4_div_2:
    1.12 -  "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
    1.13 +  "n mod 4 = Suc 0 \<Longrightarrow> even ((n - Suc 0) div 2)"
    1.14    by presburger
    1.15  
    1.16