theory More_Divides

lemma int_div_sub_1:
  "\<lbrakk> m \<ge> 1 \<rbrakk> \<Longrightarrow> (n - (1 :: int)) div m = (if m dvd n then (n div m) - 1 else n div m)" apply (subgoal_tac "m = 0 \<or> (n - (1 :: int)) div m = (if m dvd n then (n div m) - 1 else n div m)") apply fastforce apply (subst mult_cancel_right[symmetric]) apply (simp only: left_diff_distrib split: if_split) apply (simp only: mod_div_equality_div_eq) apply (clarsimp simp: field_simps) apply (clarsimp simp: dvd_eq_mod_eq_0) apply (cases "m = 1") apply simp apply (subst mod_diff_eq[symmetric], simp add: zmod_minus1) apply clarsimp apply (subst diff_add_cancel[where b=1, symmetric]) apply (subst mod_add_eq[symmetric]) apply (simp add: field_simps) apply (rule mod_pos_pos_trivial) apply (subst add_0_right[where a=0, symmetric]) apply (rule add_mono) apply simp apply simp apply (cases "(n - 1) mod m = m - 1") apply (drule zmod_helper[where a=1]) apply simp apply (subgoal_tac "1 + (n - 1) mod m \<le> m") apply simp apply (subst field_simps, rule zless_imp_add1_zle) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 \<le> m \<Longrightarrow> (n - 1) div m = (if m dvd n then n div m - 1 else n div m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 \<le> m; m = 0 \<or> (n - 1) div m = (if m dvd n then n div m - 1 else n div m)\<rbrakk> \<Longrightarrow> (n - 1) div m = (if m dvd n then n div m - 1 else n div m)
 2. 1 \<le> m \<Longrightarrow> m = 0 \<or> (n - 1) div m = (if m dvd n then n div m - 1 else n div m) proof (prove)
goal (1 subgoal):
 1. 1 \<le> m \<Longrightarrow> m = 0 \<or> (n - 1) div m = (if m dvd n then n div m - 1 else n div m) proof (prove)
goal (1 subgoal):
 1. 1 \<le> m \<Longrightarrow> (n - 1) div m * m = (if m dvd n then n div m - 1 else n div m) * m proof (prove)
goal (1 subgoal):
 1. 1 \<le> m \<Longrightarrow> (m dvd n \<longrightarrow> (n - 1) div m * m = n div m * m - 1 * m) \<and> (\<not> m dvd n \<longrightarrow> (n - 1) div m * m = n div m * m) proof (prove)
goal (1 subgoal):
 1. 1 \<le> m \<Longrightarrow> (m dvd n \<longrightarrow> n - 1 - (n - 1) mod m = n - n mod m - 1 * m) \<and> (\<not> m dvd n \<longrightarrow> n - 1 - (n - 1) mod m = n - n mod m) proof (prove)
goal (1 subgoal):
 1. 1 \<le> m \<Longrightarrow> (m dvd n \<longrightarrow> m = 1 + (n - 1) mod m) \<and> (\<not> m dvd n \<longrightarrow> n mod m = 1 + (n - 1) mod m) proof (prove)
goal (1 subgoal):
 1. 1 \<le> m \<Longrightarrow> (n mod m = 0 \<longrightarrow> m = 1 + (n - 1) mod m) \<and> (n mod m \<noteq> 0 \<longrightarrow> n mod m = 1 + (n - 1) mod m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 \<le> m; m = 1\<rbrakk> \<Longrightarrow> (n mod m = 0 \<longrightarrow> m = 1 + (n - 1) mod m) \<and> (n mod m \<noteq> 0 \<longrightarrow> n mod m = 1 + (n - 1) mod m)
 2. \<lbrakk>1 \<le> m; m \<noteq> 1\<rbrakk> \<Longrightarrow> (n mod m = 0 \<longrightarrow> m = 1 + (n - 1) mod m) \<and> (n mod m \<noteq> 0 \<longrightarrow> n mod m = 1 + (n - 1) mod m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1\<rbrakk> \<Longrightarrow> (n mod m = 0 \<longrightarrow> m = 1 + (n - 1) mod m) \<and> (n mod m \<noteq> 0 \<longrightarrow> n mod m = 1 + (n - 1) mod m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1\<rbrakk> \<Longrightarrow> n mod m \<noteq> 0 \<longrightarrow> n mod m = 1 + (n - 1) mod m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0\<rbrakk> \<Longrightarrow> n mod m = 1 + (n - 1) mod m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0\<rbrakk> \<Longrightarrow> (n - 1 + 1) mod m = 1 + (n - 1) mod m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0\<rbrakk> \<Longrightarrow> ((n - 1) mod m + 1 mod m) mod m = 1 + (n - 1) mod m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0\<rbrakk> \<Longrightarrow> (1 + (n - 1) mod m) mod m = 1 + (n - 1) mod m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0\<rbrakk> \<Longrightarrow> 0 \<le> 1 + (n - 1) mod m
 2. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0\<rbrakk> \<Longrightarrow> 1 + (n - 1) mod m < m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0\<rbrakk> \<Longrightarrow> 0 + 0 \<le> 1 + (n - 1) mod m
 2. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0\<rbrakk> \<Longrightarrow> 1 + (n - 1) mod m < m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0\<rbrakk> \<Longrightarrow> 0 \<le> 1
 2. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0\<rbrakk> \<Longrightarrow> 0 \<le> (n - 1) mod m
 3. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0\<rbrakk> \<Longrightarrow> 1 + (n - 1) mod m < m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0\<rbrakk> \<Longrightarrow> 0 \<le> (n - 1) mod m
 2. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0\<rbrakk> \<Longrightarrow> 1 + (n - 1) mod m < m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0\<rbrakk> \<Longrightarrow> 1 + (n - 1) mod m < m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0; (n - 1) mod m = m - 1\<rbrakk> \<Longrightarrow> 1 + (n - 1) mod m < m
 2. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0; (n - 1) mod m \<noteq> m - 1\<rbrakk> \<Longrightarrow> 1 + (n - 1) mod m < m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0; (n - 1 + 1) mod m = (m - 1 + 1) mod m\<rbrakk> \<Longrightarrow> 1 + (n - 1) mod m < m
 2. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0; (n - 1) mod m \<noteq> m - 1\<rbrakk> \<Longrightarrow> 1 + (n - 1) mod m < m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0; (n - 1) mod m \<noteq> m - 1\<rbrakk> \<Longrightarrow> 1 + (n - 1) mod m < m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0; (n - 1) mod m \<noteq> m - 1; 1 + (n - 1) mod m \<le> m\<rbrakk> \<Longrightarrow> 1 + (n - 1) mod m < m
 2. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0; (n - 1) mod m \<noteq> m - 1\<rbrakk> \<Longrightarrow> 1 + (n - 1) mod m \<le> m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0; (n - 1) mod m \<noteq> m - 1\<rbrakk> \<Longrightarrow> 1 + (n - 1) mod m \<le> m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> m; m \<noteq> 1; n mod m \<noteq> 0; (n - 1) mod m \<noteq> m - 1\<rbrakk> \<Longrightarrow> (n - 1) mod m < m proof (prove)
goal:
No subgoals!