src/HOL/Divides.thy

 
 end
 
 class semiring_div_parity = semiring_div + semiring_numeral +
   assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
+  assumes one_mod_two_eq_one: "1 mod 2 = 1"
 begin
 
 lemma parity_cases [case_names even odd]:
   assumes "a mod 2 = 0 \<Longrightarrow> P"
   assumes "a mod 2 = 1 \<Longrightarrow> P"

     with discrete have "1 \<le> a mod 2" by simp
     with `a mod 2 \<noteq> 1` have "1 < a mod 2" by simp
     with discrete have "2 \<le> a mod 2" by simp
     with `a mod 2 < 2` show False by simp
   qed
+next
+  show "1 mod 2 = 1"
+    by (rule mod_less) simp_all
 qed
 
 lemma divmod_digit_1:
   assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
   shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")