src/HOL/Divides.thy
changeset 58646 cd63a4b12a33
parent 58511 97aec08d6f28
child 58710 7216a10d69ba
     1.1 --- a/src/HOL/Divides.thy	Thu Oct 09 22:43:48 2014 +0200
     1.2 +++ b/src/HOL/Divides.thy	Fri Oct 10 19:55:32 2014 +0200
     1.3 @@ -506,6 +506,7 @@
     1.4  
     1.5  class semiring_div_parity = semiring_div + semiring_numeral +
     1.6    assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
     1.7 +  assumes one_mod_two_eq_one: "1 mod 2 = 1"
     1.8  begin
     1.9  
    1.10  lemma parity_cases [case_names even odd]:
    1.11 @@ -569,6 +570,9 @@
    1.12      with discrete have "2 \<le> a mod 2" by simp
    1.13      with `a mod 2 < 2` show False by simp
    1.14    qed
    1.15 +next
    1.16 +  show "1 mod 2 = 1"
    1.17 +    by (rule mod_less) simp_all
    1.18  qed
    1.19  
    1.20  lemma divmod_digit_1: