theory More_Divides

lemma diff_mod_le:
  \<open>a - a mod b \<le> d - b\<close> if \<open>a < d\<close> \<open>b dvd d\<close> for a b d :: nat using that apply(subst minus_mod_eq_mult_div) apply(clarsimp simp: dvd_def) apply(cases \<open>b = 0\<close>) apply simp apply(subgoal_tac "a div b \<le> k - 1") prefer 2 apply(subgoal_tac "a div b < k") apply(simp add: less_Suc_eq_le [symmetric]) apply(subgoal_tac "b * (a div b) < b * ((b * k) div b)") apply clarsimp apply(subst div_mult_self1_is_m) apply arith apply(rule le_less_trans) apply simp apply(subst mult.commute) apply(rule div_times_less_eq_dividend) apply assumption apply clarsimp apply(subgoal_tac "b * (a div b) \<le> b * (k - 1)") apply(erule le_trans) apply(simp add: diff_mult_distrib2) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a - a mod b \<le> d - b proof (prove)
using this:
a < d
b dvd d

goal (1 subgoal):
 1. a - a mod b \<le> d - b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < d; b dvd d\<rbrakk> \<Longrightarrow> b * (a div b) \<le> d - b proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; b = 0\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b
 2. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0; a div b \<le> k - 1\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b
 2. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0\<rbrakk> \<Longrightarrow> a div b \<le> k - 1 proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0\<rbrakk> \<Longrightarrow> a div b \<le> k - 1
 2. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0; a div b \<le> k - 1\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0; a div b < k\<rbrakk> \<Longrightarrow> a div b \<le> k - 1
 2. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0\<rbrakk> \<Longrightarrow> a div b < k
 3. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0; a div b \<le> k - 1\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0\<rbrakk> \<Longrightarrow> a div b < k
 2. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0; a div b \<le> k - 1\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0; b * (a div b) < b * (b * k div b)\<rbrakk> \<Longrightarrow> a div b < k
 2. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0\<rbrakk> \<Longrightarrow> b * (a div b) < b * (b * k div b)
 3. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0; a div b \<le> k - 1\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0\<rbrakk> \<Longrightarrow> b * (a div b) < b * (b * k div b)
 2. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0; a div b \<le> k - 1\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < b
 2. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0\<rbrakk> \<Longrightarrow> b * (a div b) < b * k
 3. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0; a div b \<le> k - 1\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0\<rbrakk> \<Longrightarrow> b * (a div b) < b * k
 2. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0; a div b \<le> k - 1\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0\<rbrakk> \<Longrightarrow> b * (a div b) \<le> ?y17 k
 2. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0\<rbrakk> \<Longrightarrow> ?y17 k < b * k
 3. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0; a div b \<le> k - 1\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; 0 < b\<rbrakk> \<Longrightarrow> b * (a div b) \<le> ?y17 k
 2. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0\<rbrakk> \<Longrightarrow> ?y17 k < b * k
 3. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0; a div b \<le> k - 1\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; 0 < b\<rbrakk> \<Longrightarrow> a div b * b \<le> ?y21 k (?k21 k)
 2. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0\<rbrakk> \<Longrightarrow> ?y21 k (?k21 k) < b * k
 3. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0; a div b \<le> k - 1\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0\<rbrakk> \<Longrightarrow> a < b * k
 2. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0; a div b \<le> k - 1\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; b \<noteq> 0; a div b \<le> k - 1\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; 0 < b; a div b \<le> k - Suc 0\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; 0 < b; a div b \<le> k - Suc 0; b * (a div b) \<le> b * (k - 1)\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * k - b
 2. \<And>k. \<lbrakk>a < b * k; d = b * k; 0 < b; a div b \<le> k - Suc 0\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * (k - 1) proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; 0 < b; a div b \<le> k - Suc 0\<rbrakk> \<Longrightarrow> b * (k - 1) \<le> b * k - b
 2. \<And>k. \<lbrakk>a < b * k; d = b * k; 0 < b; a div b \<le> k - Suc 0\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * (k - 1) proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>a < b * k; d = b * k; 0 < b; a div b \<le> k - Suc 0\<rbrakk> \<Longrightarrow> b * (a div b) \<le> b * (k - 1) proof (prove)
goal:
No subgoals!