theory Blatt8
imports Main 
begin

lemma plus_div_less_self:
  fixes a b c :: nat
  assumes "a < c" and "b < c"
  shows "(a + b) div c < c"
proof (cases "2 \<le> c")
  case True
  from assms have "a + b \<le> c + (c - 1)" by simp
  then have "(a + b) div c \<le> (c + (c - 1)) div c" by (rule div_le_mono)
  moreover have "(c + (c - 1)) div c < 2" using `2 \<le> c` 
    by (simp only: div_add_self1) simp
  ultimately have "(a + b) div c < 2" by simp
  with `2 \<le> c` show "(a + b) div c < c" by auto
next
  case False then show ?thesis using assms by simp
qed

lemma times_div_less_self:
  fixes a b c :: nat
  assumes "a < c" and "b < c"
  shows "(a * b) div c < c"
proof (cases "2 \<le> c")
  case True
  then obtain d where "c = Suc d" by (cases c) simp_all
  then have "c * c - 1 = (c - 1) + (c - 1) * c" by simp
  then have "(c * c - 1) div c = ((c - 1) + (c - 1) * c) div c" by simp
  also have "\<dots> = c - 1 + (c - 1) div c" using `c = Suc d` 
    by (simp only: div_mult_self1)
  also have "\<dots> = c - 1" using `c = Suc d` by simp
  finally have dec_c: "(c * c - 1) div c = c - 1" .
  from assms have "a * b < c * c" by (simp add: mult_strict_mono)
  then have "a * b \<le> c * c - 1" by simp
  then have "(a * b) div c \<le> (c * c - 1) div c" by (rule div_le_mono)
  with dec_c have "(a * b) div c \<le> c - 1" by simp
  then show "(a * b) div c < c" using `c = Suc d` by simp
next
  case False then have "c = 0 \<or> c = 1" by arith
  then show ?thesis using assms by simp
qed

find_theorems "(_ + _) * _ = _"
find_theorems "((_::nat) + _) * _ = _"
find_theorems "((?m::nat) + _) * _ = ?m * _ + _"