[STATEMENT]
lemma congruence_congruence_inv [simp]:
  assumes "mat_det M \<noteq> 0"
  shows "congruence M (congruence (mat_inv M) H) = H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. congruence M (congruence (mat_inv M) H) = H
[PROOF STEP]
using assms congruence_congruence[of M "mat_inv M" H]
[PROOF STATE]
proof (prove)
using this:
mat_det M \<noteq> 0
congruence M (congruence (mat_inv M) H) = congruence (mat_inv M *\<^sub>m\<^sub>m M) H

goal (1 subgoal):
 1. congruence M (congruence (mat_inv M) H) = H
[PROOF STEP]
using mat_inv_l[of M] mat_eye_l mat_eye_r
[PROOF STATE]
proof (prove)
using this:
mat_det M \<noteq> 0
congruence M (congruence (mat_inv M) H) = congruence (mat_inv M *\<^sub>m\<^sub>m M) H
mat_det M \<noteq> 0 \<Longrightarrow> mat_inv M *\<^sub>m\<^sub>m M = eye
eye *\<^sub>m\<^sub>m ?A = ?A
?A *\<^sub>m\<^sub>m eye = ?A

goal (1 subgoal):
 1. congruence M (congruence (mat_inv M) H) = H
[PROOF STEP]
unfolding congruence_def
[PROOF STATE]
proof (prove)
using this:
mat_det M \<noteq> 0
mat_adj M *\<^sub>m\<^sub>m (mat_adj (mat_inv M) *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m mat_inv M) *\<^sub>m\<^sub>m M = mat_adj (mat_inv M *\<^sub>m\<^sub>m M) *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m (mat_inv M *\<^sub>m\<^sub>m M)
mat_det M \<noteq> 0 \<Longrightarrow> mat_inv M *\<^sub>m\<^sub>m M = eye
eye *\<^sub>m\<^sub>m ?A = ?A
?A *\<^sub>m\<^sub>m eye = ?A

goal (1 subgoal):
 1. mat_adj M *\<^sub>m\<^sub>m (mat_adj (mat_inv M) *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m mat_inv M) *\<^sub>m\<^sub>m M = H
[PROOF STEP]
by (simp del: eye_def)


[STATEMENT]
lemma congruence_inv:
  assumes "mat_det M \<noteq> 0" and "congruence M H = H'"
  shows "congruence (mat_inv M) H' = H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. congruence (mat_inv M) H' = H
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat_det M \<noteq> 0
congruence M H = H'

goal (1 subgoal):
 1. congruence (mat_inv M) H' = H
[PROOF STEP]
using \<open>mat_det M \<noteq> 0\<close> mult_mm_inv_l[of "mat_adj M" "H *\<^sub>m\<^sub>m M" "H'"]
[PROOF STATE]
proof (prove)
using this:
mat_det M \<noteq> 0
congruence M H = H'
mat_det M \<noteq> 0
\<lbrakk>mat_det (mat_adj M) \<noteq> 0; mat_adj M *\<^sub>m\<^sub>m (H *\<^sub>m\<^sub>m M) = H'\<rbrakk> \<Longrightarrow> H *\<^sub>m\<^sub>m M = mat_inv (mat_adj M) *\<^sub>m\<^sub>m H'

goal (1 subgoal):
 1. congruence (mat_inv M) H' = H
[PROOF STEP]
using mult_mm_inv_r[of M "H" "mat_inv (mat_adj M) *\<^sub>m\<^sub>m H'"]
[PROOF STATE]
proof (prove)
using this:
mat_det M \<noteq> 0
congruence M H = H'
mat_det M \<noteq> 0
\<lbrakk>mat_det (mat_adj M) \<noteq> 0; mat_adj M *\<^sub>m\<^sub>m (H *\<^sub>m\<^sub>m M) = H'\<rbrakk> \<Longrightarrow> H *\<^sub>m\<^sub>m M = mat_inv (mat_adj M) *\<^sub>m\<^sub>m H'
\<lbrakk>mat_det M \<noteq> 0; H *\<^sub>m\<^sub>m M = mat_inv (mat_adj M) *\<^sub>m\<^sub>m H'\<rbrakk> \<Longrightarrow> H = mat_inv (mat_adj M) *\<^sub>m\<^sub>m H' *\<^sub>m\<^sub>m mat_inv M

goal (1 subgoal):
 1. congruence (mat_inv M) H' = H
[PROOF STEP]
by (simp add: mat_det_adj mult_mm_assoc mat_adj_inv)


[STATEMENT]
lemma congruence_scale_m [simp]:
  shows "congruence M (k *\<^sub>s\<^sub>m H) = k *\<^sub>s\<^sub>m (congruence M H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. congruence M (k *\<^sub>s\<^sub>m H) = k *\<^sub>s\<^sub>m congruence M H
[PROOF STEP]
by (cases M, cases H) (auto simp add: mat_adj_def mat_cnj_def field_simps)


[STATEMENT]
lemma inj_congruence:
  assumes "mat_det M \<noteq> 0" and "congruence M H = congruence M H'"
  shows "H = H'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H = H'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H = H'
[PROOF STEP]
have "H *\<^sub>m\<^sub>m M = H' *\<^sub>m\<^sub>m M "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H *\<^sub>m\<^sub>m M = H' *\<^sub>m\<^sub>m M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat_det M \<noteq> 0
congruence M H = congruence M H'

goal (1 subgoal):
 1. H *\<^sub>m\<^sub>m M = H' *\<^sub>m\<^sub>m M
[PROOF STEP]
using mult_mm_cancel_l[of "mat_adj M" "H *\<^sub>m\<^sub>m M" "H' *\<^sub>m\<^sub>m M"]
[PROOF STATE]
proof (prove)
using this:
mat_det M \<noteq> 0
congruence M H = congruence M H'
\<lbrakk>mat_det (mat_adj M) \<noteq> 0; mat_adj M *\<^sub>m\<^sub>m (H *\<^sub>m\<^sub>m M) = mat_adj M *\<^sub>m\<^sub>m (H' *\<^sub>m\<^sub>m M)\<rbrakk> \<Longrightarrow> H *\<^sub>m\<^sub>m M = H' *\<^sub>m\<^sub>m M

goal (1 subgoal):
 1. H *\<^sub>m\<^sub>m M = H' *\<^sub>m\<^sub>m M
[PROOF STEP]
by (simp add: mat_det_adj mult_mm_assoc)
[PROOF STATE]
proof (state)
this:
H *\<^sub>m\<^sub>m M = H' *\<^sub>m\<^sub>m M

goal (1 subgoal):
 1. H = H'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
H *\<^sub>m\<^sub>m M = H' *\<^sub>m\<^sub>m M

goal (1 subgoal):
 1. H = H'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
H *\<^sub>m\<^sub>m M = H' *\<^sub>m\<^sub>m M
mat_det M \<noteq> 0
congruence M H = congruence M H'

goal (1 subgoal):
 1. H = H'
[PROOF STEP]
using mult_mm_cancel_r[of "M" "H" "H'"]
[PROOF STATE]
proof (prove)
using this:
H *\<^sub>m\<^sub>m M = H' *\<^sub>m\<^sub>m M
mat_det M \<noteq> 0
congruence M H = congruence M H'
\<lbrakk>mat_det M \<noteq> 0; H *\<^sub>m\<^sub>m M = H' *\<^sub>m\<^sub>m M\<rbrakk> \<Longrightarrow> H = H'

goal (1 subgoal):
 1. H = H'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
H = H'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_det_congruence [simp]:
  "mat_det (congruence M H) = (cor ((cmod (mat_det M))\<^sup>2)) * mat_det H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_det (congruence M H) = cor ((cmod (mat_det M))\<^sup>2) * mat_det H
[PROOF STEP]
using complex_mult_cnj_cmod[of "mat_det M"]
[PROOF STATE]
proof (prove)
using this:
mat_det M * cnj (mat_det M) = cor ((cmod (mat_det M))\<^sup>2)

goal (1 subgoal):
 1. mat_det (congruence M H) = cor ((cmod (mat_det M))\<^sup>2) * mat_det H
[PROOF STEP]
by (auto simp add: mat_det_adj field_simps)


[STATEMENT]
lemma det_sgn_congruence [simp]:
  assumes "mat_det M \<noteq> 0"
  shows "sgn (mat_det (congruence M H)) = sgn (mat_det H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn (mat_det (congruence M H)) = sgn (mat_det H)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat_det M \<noteq> 0

goal (1 subgoal):
 1. sgn (mat_det (congruence M H)) = sgn (mat_det H)
[PROOF STEP]
by (subst mat_det_congruence, auto simp add: sgn_mult power2_eq_square) (simp add: sgn_of_real)


[STATEMENT]
lemma Re_det_sgn_congruence [simp]:
  assumes "mat_det M \<noteq> 0"
  shows "sgn (Re (mat_det (congruence M H))) = sgn (Re (mat_det H))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn (Re (mat_det (congruence M H))) = sgn (Re (mat_det H))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sgn (Re (mat_det (congruence M H))) = sgn (Re (mat_det H))
[PROOF STEP]
have *: "Re (mat_det (congruence M H)) = (cmod (mat_det M))\<^sup>2 * Re (mat_det H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re (mat_det (congruence M H)) = (cmod (mat_det M))\<^sup>2 * Re (mat_det H)
[PROOF STEP]
by (subst mat_det_congruence, subst Re_mult_real, rule Im_complex_of_real) (subst Re_complex_of_real, simp)
[PROOF STATE]
proof (state)
this:
Re (mat_det (congruence M H)) = (cmod (mat_det M))\<^sup>2 * Re (mat_det H)

goal (1 subgoal):
 1. sgn (Re (mat_det (congruence M H))) = sgn (Re (mat_det H))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn (Re (mat_det (congruence M H))) = sgn (Re (mat_det H))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat_det M \<noteq> 0

goal (1 subgoal):
 1. sgn (Re (mat_det (congruence M H))) = sgn (Re (mat_det H))
[PROOF STEP]
by (subst *) (auto simp add: sgn_mult)
[PROOF STATE]
proof (state)
this:
sgn (Re (mat_det (congruence M H))) = sgn (Re (mat_det H))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bilinear_form_congruence [simp]:
  assumes "mat_det M \<noteq> 0"
  shows "bilinear_form (M *\<^sub>m\<^sub>v v1) (M *\<^sub>m\<^sub>v v2) (congruence (mat_inv M) H) =
         bilinear_form v1 v2 H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bilinear_form (M *\<^sub>m\<^sub>v v1) (M *\<^sub>m\<^sub>v v2) (congruence (mat_inv M) H) = bilinear_form v1 v2 H
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bilinear_form (M *\<^sub>m\<^sub>v v1) (M *\<^sub>m\<^sub>v v2) (congruence (mat_inv M) H) = bilinear_form v1 v2 H
[PROOF STEP]
have "mat_det (mat_adj M) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_det (mat_adj M) \<noteq> 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat_det M \<noteq> 0

goal (1 subgoal):
 1. mat_det (mat_adj M) \<noteq> 0
[PROOF STEP]
by (simp add: mat_det_adj)
[PROOF STATE]
proof (state)
this:
mat_det (mat_adj M) \<noteq> 0

goal (1 subgoal):
 1. bilinear_form (M *\<^sub>m\<^sub>v v1) (M *\<^sub>m\<^sub>v v2) (congruence (mat_inv M) H) = bilinear_form v1 v2 H
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bilinear_form (M *\<^sub>m\<^sub>v v1) (M *\<^sub>m\<^sub>v v2) (congruence (mat_inv M) H) = bilinear_form v1 v2 H
[PROOF STEP]
unfolding bilinear_form_def congruence_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_cnj (M *\<^sub>m\<^sub>v v1) *\<^sub>v\<^sub>m (mat_adj (mat_inv M) *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m mat_inv M) *\<^sub>v\<^sub>v (M *\<^sub>m\<^sub>v v2) = vec_cnj v1 *\<^sub>v\<^sub>m H *\<^sub>v\<^sub>v v2
[PROOF STEP]
apply (subst mult_mv_mult_vm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_cnj (v1 *\<^sub>v\<^sub>m mat_transpose M) *\<^sub>v\<^sub>m (mat_adj (mat_inv M) *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m mat_inv M) *\<^sub>v\<^sub>v (M *\<^sub>m\<^sub>v v2) = vec_cnj v1 *\<^sub>v\<^sub>m H *\<^sub>v\<^sub>v v2
[PROOF STEP]
apply (subst vec_cnj_mult_vm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_cnj v1 *\<^sub>v\<^sub>m mat_cnj (mat_transpose M) *\<^sub>v\<^sub>m (mat_adj (mat_inv M) *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m mat_inv M) *\<^sub>v\<^sub>v (M *\<^sub>m\<^sub>v v2) = vec_cnj v1 *\<^sub>v\<^sub>m H *\<^sub>v\<^sub>v v2
[PROOF STEP]
apply (subst mat_adj_def[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_cnj v1 *\<^sub>v\<^sub>m mat_adj M *\<^sub>v\<^sub>m (mat_adj (mat_inv M) *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m mat_inv M) *\<^sub>v\<^sub>v (M *\<^sub>m\<^sub>v v2) = vec_cnj v1 *\<^sub>v\<^sub>m H *\<^sub>v\<^sub>v v2
[PROOF STEP]
apply (subst mult_vm_vm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_cnj v1 *\<^sub>v\<^sub>m (mat_adj M *\<^sub>m\<^sub>m (mat_adj (mat_inv M) *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m mat_inv M)) *\<^sub>v\<^sub>v (M *\<^sub>m\<^sub>v v2) = vec_cnj v1 *\<^sub>v\<^sub>m H *\<^sub>v\<^sub>v v2
[PROOF STEP]
apply (subst mult_vv_mv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_cnj v1 *\<^sub>v\<^sub>m (mat_adj M *\<^sub>m\<^sub>m (mat_adj (mat_inv M) *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m mat_inv M)) *\<^sub>v\<^sub>m M *\<^sub>v\<^sub>v v2 = vec_cnj v1 *\<^sub>v\<^sub>m H *\<^sub>v\<^sub>v v2
[PROOF STEP]
apply (subst mult_vm_vm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_cnj v1 *\<^sub>v\<^sub>m (mat_adj M *\<^sub>m\<^sub>m (mat_adj (mat_inv M) *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m mat_inv M) *\<^sub>m\<^sub>m M) *\<^sub>v\<^sub>v v2 = vec_cnj v1 *\<^sub>v\<^sub>m H *\<^sub>v\<^sub>v v2
[PROOF STEP]
apply (subst mat_adj_inv[OF \<open>mat_det M \<noteq> 0\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_cnj v1 *\<^sub>v\<^sub>m (mat_adj M *\<^sub>m\<^sub>m (mat_inv (mat_adj M) *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m mat_inv M) *\<^sub>m\<^sub>m M) *\<^sub>v\<^sub>v v2 = vec_cnj v1 *\<^sub>v\<^sub>m H *\<^sub>v\<^sub>v v2
[PROOF STEP]
apply (subst mult_assoc_5)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_cnj v1 *\<^sub>v\<^sub>m (mat_adj M *\<^sub>m\<^sub>m mat_inv (mat_adj M) *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m (mat_inv M *\<^sub>m\<^sub>m M)) *\<^sub>v\<^sub>v v2 = vec_cnj v1 *\<^sub>v\<^sub>m H *\<^sub>v\<^sub>v v2
[PROOF STEP]
apply (subst mat_inv_r[OF \<open>mat_det (mat_adj M) \<noteq> 0\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_cnj v1 *\<^sub>v\<^sub>m (eye *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m (mat_inv M *\<^sub>m\<^sub>m M)) *\<^sub>v\<^sub>v v2 = vec_cnj v1 *\<^sub>v\<^sub>m H *\<^sub>v\<^sub>v v2
[PROOF STEP]
apply (subst mat_inv_l[OF \<open>mat_det M \<noteq> 0\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_cnj v1 *\<^sub>v\<^sub>m (eye *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m eye) *\<^sub>v\<^sub>v v2 = vec_cnj v1 *\<^sub>v\<^sub>m H *\<^sub>v\<^sub>v v2
[PROOF STEP]
apply (subst mat_eye_l, subst mat_eye_r)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_cnj v1 *\<^sub>v\<^sub>m H *\<^sub>v\<^sub>v v2 = vec_cnj v1 *\<^sub>v\<^sub>m H *\<^sub>v\<^sub>v v2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bilinear_form (M *\<^sub>m\<^sub>v v1) (M *\<^sub>m\<^sub>v v2) (congruence (mat_inv M) H) = bilinear_form v1 v2 H

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quad_form_congruence [simp]:
  assumes "mat_det M \<noteq> 0"
  shows "quad_form (M *\<^sub>m\<^sub>v z) (congruence (mat_inv M) H) = quad_form z H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quad_form (M *\<^sub>m\<^sub>v z) (congruence (mat_inv M) H) = quad_form z H
[PROOF STEP]
using bilinear_form_congruence[OF assms]
[PROOF STATE]
proof (prove)
using this:
bilinear_form (M *\<^sub>m\<^sub>v ?v1.0) (M *\<^sub>m\<^sub>v ?v2.0) (congruence (mat_inv M) ?H) = bilinear_form ?v1.0 ?v2.0 ?H

goal (1 subgoal):
 1. quad_form (M *\<^sub>m\<^sub>v z) (congruence (mat_inv M) H) = quad_form z H
[PROOF STEP]
by simp


[STATEMENT]
lemma mat_det_similarity [simp]:
  assumes "mat_det A \<noteq> 0"
  shows "mat_det (similarity A M) = mat_det M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_det (similarity A M) = mat_det M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat_det A \<noteq> 0

goal (1 subgoal):
 1. mat_det (similarity A M) = mat_det M
[PROOF STEP]
unfolding similarity_def
[PROOF STATE]
proof (prove)
using this:
mat_det A \<noteq> 0

goal (1 subgoal):
 1. mat_det (mat_inv A *\<^sub>m\<^sub>m M *\<^sub>m\<^sub>m A) = mat_det M
[PROOF STEP]
by (simp add: mat_det_inv)


[STATEMENT]
lemma mat_trace_similarity [simp]:
  assumes "mat_det A \<noteq> 0"
  shows "mat_trace (similarity A M) = mat_trace M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_trace (similarity A M) = mat_trace M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_trace (similarity A M) = mat_trace M
[PROOF STEP]
obtain a b c d where AA: "A = (a, b, c, d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b c d. A = (a, b, c, d) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases A) auto
[PROOF STATE]
proof (state)
this:
A = (a, b, c, d)

goal (1 subgoal):
 1. mat_trace (similarity A M) = mat_trace M
[PROOF STEP]
obtain mA mB mC mD where MM: "M = (mA, mB, mC, mD)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>mA mB mC mD. M = (mA, mB, mC, mD) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases M) auto
[PROOF STATE]
proof (state)
this:
M = (mA, mB, mC, mD)

goal (1 subgoal):
 1. mat_trace (similarity A M) = mat_trace M
[PROOF STEP]
have "mA * (a * d) / (a * d - b * c) + mD * (a * d) / (a * d - b * c) =
        mA + mD + mA * (b * c) / (a * d - b * c) + mD * (b * c) / (a * d - b * c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mA * (a * d) / (a * d - b * c) + mD * (a * d) / (a * d - b * c) = mA + mD + mA * (b * c) / (a * d - b * c) + mD * (b * c) / (a * d - b * c)
[PROOF STEP]
using assms AA
[PROOF STATE]
proof (prove)
using this:
mat_det A \<noteq> 0
A = (a, b, c, d)

goal (1 subgoal):
 1. mA * (a * d) / (a * d - b * c) + mD * (a * d) / (a * d - b * c) = mA + mD + mA * (b * c) / (a * d - b * c) + mD * (b * c) / (a * d - b * c)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
mA * (a * d) / (a * d - b * c) + mD * (a * d) / (a * d - b * c) = mA + mD + mA * (b * c) / (a * d - b * c) + mD * (b * c) / (a * d - b * c)

goal (1 subgoal):
 1. mat_trace (similarity A M) = mat_trace M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mA * (a * d) / (a * d - b * c) + mD * (a * d) / (a * d - b * c) = mA + mD + mA * (b * c) / (a * d - b * c) + mD * (b * c) / (a * d - b * c)

goal (1 subgoal):
 1. mat_trace (similarity A M) = mat_trace M
[PROOF STEP]
using AA MM
[PROOF STATE]
proof (prove)
using this:
mA * (a * d) / (a * d - b * c) + mD * (a * d) / (a * d - b * c) = mA + mD + mA * (b * c) / (a * d - b * c) + mD * (b * c) / (a * d - b * c)
A = (a, b, c, d)
M = (mA, mB, mC, mD)

goal (1 subgoal):
 1. mat_trace (similarity A M) = mat_trace M
[PROOF STEP]
by (simp add: field_simps similarity_def)
[PROOF STATE]
proof (state)
this:
mat_trace (similarity A M) = mat_trace M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma similarity_eye [simp]:
  shows "similarity eye M = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. similarity eye M = M
[PROOF STEP]
unfolding similarity_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_inv eye *\<^sub>m\<^sub>m M *\<^sub>m\<^sub>m eye = M
[PROOF STEP]
using mat_eye_l mat_eye_r
[PROOF STATE]
proof (prove)
using this:
eye *\<^sub>m\<^sub>m ?A = ?A
?A *\<^sub>m\<^sub>m eye = ?A

goal (1 subgoal):
 1. mat_inv eye *\<^sub>m\<^sub>m M *\<^sub>m\<^sub>m eye = M
[PROOF STEP]
by auto


[STATEMENT]
lemma similarity_eye' [simp]:
  shows "similarity (1, 0, 0, 1) M = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. similarity (1, 0, 0, 1) M = M
[PROOF STEP]
unfolding eye_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. similarity eye M = M
[PROOF STEP]
by (simp del: eye_def)


[STATEMENT]
lemma similarity_comp [simp]:
  assumes "mat_det A1 \<noteq> 0" and "mat_det A2 \<noteq> 0"
  shows "similarity A1 (similarity A2 M) = similarity (A2*\<^sub>m\<^sub>mA1) M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. similarity A1 (similarity A2 M) = similarity (A2 *\<^sub>m\<^sub>m A1) M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat_det A1 \<noteq> 0
mat_det A2 \<noteq> 0

goal (1 subgoal):
 1. similarity A1 (similarity A2 M) = similarity (A2 *\<^sub>m\<^sub>m A1) M
[PROOF STEP]
unfolding similarity_def
[PROOF STATE]
proof (prove)
using this:
mat_det A1 \<noteq> 0
mat_det A2 \<noteq> 0

goal (1 subgoal):
 1. mat_inv A1 *\<^sub>m\<^sub>m (mat_inv A2 *\<^sub>m\<^sub>m M *\<^sub>m\<^sub>m A2) *\<^sub>m\<^sub>m A1 = mat_inv (A2 *\<^sub>m\<^sub>m A1) *\<^sub>m\<^sub>m M *\<^sub>m\<^sub>m (A2 *\<^sub>m\<^sub>m A1)
[PROOF STEP]
by (simp add: mult_mm_assoc mat_inv_mult_mm)


[STATEMENT]
lemma similarity_inv:
  assumes "similarity A M1 = M2" and "mat_det A \<noteq> 0"
  shows "similarity (mat_inv A) M2 = M1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. similarity (mat_inv A) M2 = M1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
similarity A M1 = M2
mat_det A \<noteq> 0

goal (1 subgoal):
 1. similarity (mat_inv A) M2 = M1
[PROOF STEP]
unfolding similarity_def
[PROOF STATE]
proof (prove)
using this:
mat_inv A *\<^sub>m\<^sub>m M1 *\<^sub>m\<^sub>m A = M2
mat_det A \<noteq> 0

goal (1 subgoal):
 1. mat_inv (mat_inv A) *\<^sub>m\<^sub>m M2 *\<^sub>m\<^sub>m mat_inv A = M1
[PROOF STEP]
by (metis mat_det_mult mult_mm_assoc mult_mm_inv_l mult_mm_inv_r mult_zero_left)


[STATEMENT]
lemma plus_stream_shd: "shd (x + y) = shd x + shd y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shd (x + y) = shd x + shd y
[PROOF STEP]
unfolding plus_stream_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shd (Applicative.ap (Applicative.ap (pure (+)) x) y) = shd x + shd y
[PROOF STEP]
by simp


[STATEMENT]
lemma plus_stream_stl: "stl (x + y) = stl x + stl y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stl (x + y) = stl x + stl y
[PROOF STEP]
unfolding plus_stream_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stl (Applicative.ap (Applicative.ap (pure (+)) x) y) = Applicative.ap (Applicative.ap (pure (+)) (stl x)) (stl y)
[PROOF STEP]
by simp


[STATEMENT]
lemma pure_stream_inject [simp]: "sconst x = sconst y \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pure x = pure y) = (x = y)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pure x = pure y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> pure x = pure y
[PROOF STEP]
assume "sconst x = sconst y"
[PROOF STATE]
proof (state)
this:
pure x = pure y

goal (2 subgoals):
 1. pure x = pure y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> pure x = pure y
[PROOF STEP]
hence "shd (sconst x) = shd (sconst y)"
[PROOF STATE]
proof (prove)
using this:
pure x = pure y

goal (1 subgoal):
 1. shd (pure x) = shd (pure y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
shd (pure x) = shd (pure y)

goal (2 subgoals):
 1. pure x = pure y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> pure x = pure y
[PROOF STEP]
thus "x = y"
[PROOF STATE]
proof (prove)
using this:
shd (pure x) = shd (pure y)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. x = y \<Longrightarrow> pure x = pure y
[PROOF STEP]
qed auto


[STATEMENT]
lemma of_nat_stream [applicative_unfold]: "of_nat n = sconst (of_nat n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat n = pure (of_nat n)
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. of_nat 0 = sconst (of_nat 0)
 2. \<And>n. of_nat n = sconst (of_nat n) \<Longrightarrow> of_nat (Suc n) = sconst (of_nat (Suc n))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. of_nat 0 = sconst (of_nat 0)
 2. \<And>n. of_nat n = sconst (of_nat n) \<Longrightarrow> of_nat (Suc n) = sconst (of_nat (Suc n))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat 0 = sconst (of_nat 0)
[PROOF STEP]
by (simp add: zero_stream_def del: id_apply)
[PROOF STATE]
proof (state)
this:
of_nat 0 = sconst (of_nat 0)

goal (1 subgoal):
 1. \<And>n. of_nat n = sconst (of_nat n) \<Longrightarrow> of_nat (Suc n) = sconst (of_nat (Suc n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. of_nat n = sconst (of_nat n) \<Longrightarrow> of_nat (Suc n) = sconst (of_nat (Suc n))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
of_nat n = sconst (of_nat n)

goal (1 subgoal):
 1. \<And>n. of_nat n = sconst (of_nat n) \<Longrightarrow> of_nat (Suc n) = sconst (of_nat (Suc n))
[PROOF STEP]
have "1 + pure (of_nat n) = pure (1 + of_nat n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + pure (of_nat n) = pure ((1::'b) + of_nat n)
[PROOF STEP]
by applicative_nf rule
[PROOF STATE]
proof (state)
this:
1 + pure (of_nat n) = pure ((1::?'b1) + of_nat n)

goal (1 subgoal):
 1. \<And>n. of_nat n = sconst (of_nat n) \<Longrightarrow> of_nat (Suc n) = sconst (of_nat (Suc n))
[PROOF STEP]
with Suc.IH
[PROOF STATE]
proof (chain)
picking this:
of_nat n = sconst (of_nat n)
1 + pure (of_nat n) = pure ((1::?'b1) + of_nat n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
of_nat n = sconst (of_nat n)
1 + pure (of_nat n) = pure ((1::?'b1) + of_nat n)

goal (1 subgoal):
 1. of_nat (Suc n) = sconst (of_nat (Suc n))
[PROOF STEP]
by (simp del: id_apply)
[PROOF STATE]
proof (state)
this:
of_nat (Suc n) = sconst (of_nat (Suc n))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pure_stream_numeral [applicative_unfold]: "numeral n = pure (numeral n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. numeral n = pure (numeral n)
[PROOF STEP]
by(induction n)(simp_all only: numeral.simps one_stream_def plus_stream_def ap_stream_homo)


[STATEMENT]
lemma [code_unfold]:
  fixes literal :: Literal and clause :: Clause
  shows "literal el clause = List.member clause literal"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. literal el clause = List.member clause literal
[PROOF STEP]
by (auto simp add: member_def)


[STATEMENT]
lemma wb_ctor_prism_intro:
  assumes
    "\<And> v. disc (ctor v)"
    "\<And> v. sel (ctor v) = v"
    "\<And> s. disc s \<Longrightarrow> ctor (sel s) = s"
  shows "wb_prism (ctor_prism ctor disc sel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wb_prism (ctor_prism ctor disc sel)
[PROOF STEP]
by (unfold_locales, simp_all add: lens_defs assms)
     (metis assms(3) option.distinct(1) option.sel)


[STATEMENT]
lemma ctor_codep_intro:
  assumes "\<And> x y. ctor1 x \<noteq> ctor2 y"
  shows "ctor_prism ctor1 disc1 sel1 \<nabla> ctor_prism ctor2 disc2 sel2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ctor_prism ctor1 disc1 sel1 \<nabla> ctor_prism ctor2 disc2 sel2
[PROOF STEP]
by (rule prism_diff_intro, simp add: lens_defs assms)


[STATEMENT]
lemma samp_uni_set_spmf [simp]: "set_spmf (sample_uniform q) = {..< q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_spmf (sample_uniform q) = {..<q}
[PROOF STEP]
by(simp add: sample_uniform_def)


[STATEMENT]
lemma minus_mod:
  assumes "a > b"
  shows "[a - b mod q = a - b] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a - b mod q = a - b] (mod q)
[PROOF STEP]
by(metis cong_diff_nat  cong_def le_trans less_or_eq_imp_le assms mod_less_eq_dividend mod_mod_trivial)


[STATEMENT]
lemma q_cong:"[a = q + a] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a = q + a] (mod q)
[PROOF STEP]
by (simp add: cong_def)


[STATEMENT]
lemma q_cong_reverse: "[q + a = a] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [q + a = a] (mod q)
[PROOF STEP]
by (simp add: cong_def)


[STATEMENT]
lemma qq_cong: "[a = q*q + a] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a = q * q + a] (mod q)
[PROOF STEP]
by (simp add: cong_def)


[STATEMENT]
lemma minus_q_mult_cancel:
  assumes "[a = e + b - q * c - d] (mod q)"
    and "e + b - d > 0"
    and "e + b - q * c - d > 0"
  shows  "[a = e + b  - d] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a = e + b - d] (mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [a = e + b - d] (mod q)
[PROOF STEP]
have "a mod q = (e + b - q * c - d) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod q = (e + b - q * c - d) mod q
[PROOF STEP]
using assms(1) cong_def
[PROOF STATE]
proof (prove)
using this:
[a = e + b - q * c - d] (mod q)
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)

goal (1 subgoal):
 1. a mod q = (e + b - q * c - d) mod q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a mod q = (e + b - q * c - d) mod q

goal (1 subgoal):
 1. [a = e + b - d] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod q = (e + b - q * c - d) mod q
[PROOF STEP]
have "a mod q = (e + b - d) mod q"
[PROOF STATE]
proof (prove)
using this:
a mod q = (e + b - q * c - d) mod q

goal (1 subgoal):
 1. a mod q = (e + b - d) mod q
[PROOF STEP]
by (metis (no_types) add_cancel_left_left assms(3) diff_commute diff_is_0_eq' linordered_semidom_class.add_diff_inverse mod_add_left_eq mod_mult_self1_is_0 nat_less_le)
[PROOF STATE]
proof (state)
this:
a mod q = (e + b - d) mod q

goal (1 subgoal):
 1. [a = e + b - d] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod q = (e + b - d) mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a mod q = (e + b - d) mod q

goal (1 subgoal):
 1. [a = e + b - d] (mod q)
[PROOF STEP]
using cong_def
[PROOF STATE]
proof (prove)
using this:
a mod q = (e + b - d) mod q
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)

goal (1 subgoal):
 1. [a = e + b - d] (mod q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[a = e + b - d] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma s1_s2:
  assumes "x < q" "a < q" "b < q" and r:"r < q" "y < q"
  shows "((x + a) mod q * b + q - (a * b + q - r) mod q) mod q =
          (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x + a) mod q * b + q - (a * b + q - r) mod q) mod q = (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((x + a) mod q * b + q - (a * b + q - r) mod q) mod q = (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q
[PROOF STEP]
have s: "(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q
                 = ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q
[PROOF STEP]
have lhs: "(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x*b + r) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
let ?h = "(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
have "[?h = x * y + q - (x * ((y + (q - b)) mod q) + (q - r)) mod q] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * y + q - (x * ((y + (q - b)) mod q) + (q - r)) mod q] (mod q)
[PROOF STEP]
by(simp add: assms(1) cong_def q_gt_0)
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * y + q - (x * ((y + (q - b)) mod q) + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * y + q - (x * ((y + (q - b)) mod q) + (q - r)) mod q] (mod q)
[PROOF STEP]
have "[?h = x * y + q - (x * (y + (q - b)) + (q - r)) mod q] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * y + q - (x * ((y + (q - b)) mod q) + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * y + q - (x * (y + (q - b)) + (q - r)) mod q] (mod q)
[PROOF STEP]
by (metis mod_add_left_eq mod_mult_right_eq)
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * y + q - (x * (y + (q - b)) + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * y + q - (x * (y + (q - b)) + (q - r)) mod q] (mod q)
[PROOF STEP]
have no_qq: "[?h = x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * y + q - (x * (y + (q - b)) + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)
[PROOF STEP]
by(metis distrib_left)
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)
[PROOF STEP]
have "[?h = q*q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q) \<Longrightarrow> [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)
[PROOF STEP]
have "[x * y + q - (x * y + x * (q - b) + (q - r)) mod q = q*q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x * y + q - (x * y + x * (q - b) + (q - r)) mod q = q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)
[PROOF STEP]
by (smt qq_cong  add.assoc cong_diff_nat cong_def le_add2 le_trans mod_le_divisor q_gt_0)
[PROOF STATE]
proof (state)
this:
[x * y + q - (x * y + x * (q - b) + (q - r)) mod q = q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q) \<Longrightarrow> [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[x * y + q - (x * y + x * (q - b) + (q - r)) mod q = q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[x * y + q - (x * y + x * (q - b) + (q - r)) mod q = q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)
[PROOF STEP]
using cong_trans no_qq
[PROOF STATE]
proof (prove)
using this:
[x * y + q - (x * y + x * (q - b) + (q - r)) mod q = q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)
\<lbrakk>[?b = ?c] (mod ?a); [?c = ?d] (mod ?a)\<rbrakk> \<Longrightarrow> [?b = ?d] (mod ?a)
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)
[PROOF STEP]
have mod: "[?h = q + q*q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)
[PROOF STEP]
by (smt Nat.add_diff_assoc cong_def add.assoc add.commute le_add2 le_trans mod_add_self2 mod_le_divisor q_gt_0)
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)
[PROOF STEP]
have "[?h = q + q*q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q) \<Longrightarrow> [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)
[PROOF STEP]
have 1: "q \<ge> q - b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q - b \<le> q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x < q
a < q
b < q
r < q
y < q

goal (1 subgoal):
 1. q - b \<le> q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q - b \<le> q

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q) \<Longrightarrow> [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q - b \<le> q
[PROOF STEP]
have  "q*q \<ge> x*(q-b)" "q \<ge> q - r"
[PROOF STATE]
proof (prove)
using this:
q - b \<le> q

goal (1 subgoal):
 1. x * (q - b) \<le> q * q &&& q - r \<le> q
[PROOF STEP]
using 1  assms
[PROOF STATE]
proof (prove)
using this:
q - b \<le> q
q - b \<le> q
x < q
a < q
b < q
r < q
y < q

goal (1 subgoal):
 1. x * (q - b) \<le> q * q &&& q - r \<le> q
[PROOF STEP]
apply (auto simp add: mult_strict_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < q; a < q; b < q; r < q; y < q\<rbrakk> \<Longrightarrow> x * (q - b) \<le> q * q
[PROOF STEP]
by (simp add: mult_le_mono)
[PROOF STATE]
proof (state)
this:
x * (q - b) \<le> q * q
q - r \<le> q

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q) \<Longrightarrow> [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x * (q - b) \<le> q * q
q - r \<le> q
[PROOF STEP]
have "q + q*q + x * y + q  > x * y + x * (q - b) + (q - r)"
[PROOF STATE]
proof (prove)
using this:
x * (q - b) \<le> q * q
q - r \<le> q

goal (1 subgoal):
 1. x * y + x * (q - b) + (q - r) < q + q * q + x * y + q
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
x * (q - b) \<le> q * q
q - r \<le> q
y < q

goal (1 subgoal):
 1. x * y + x * (q - b) + (q - r) < q + q * q + x * y + q
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
x * y + x * (q - b) + (q - r) < q + q * q + x * y + q

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q) \<Longrightarrow> [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x * y + x * (q - b) + (q - r) < q + q * q + x * y + q
[PROOF STEP]
have "[q + q*q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q = q + q*q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)"
[PROOF STATE]
proof (prove)
using this:
x * y + x * (q - b) + (q - r) < q + q * q + x * y + q

goal (1 subgoal):
 1. [q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)
[PROOF STEP]
using minus_mod
[PROOF STATE]
proof (prove)
using this:
x * y + x * (q - b) + (q - r) < q + q * q + x * y + q
?b < ?a \<Longrightarrow> [?a - ?b mod q = ?a - ?b] (mod q)

goal (1 subgoal):
 1. [q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q) \<Longrightarrow> [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)
[PROOF STEP]
using mod
[PROOF STATE]
proof (prove)
using this:
[q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)
[PROOF STEP]
using cong_trans
[PROOF STATE]
proof (prove)
using this:
[q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r)) mod q] (mod q)
\<lbrakk>[?b = ?c] (mod ?a); [?c = ?d] (mod ?a)\<rbrakk> \<Longrightarrow> [?b = ?d] (mod ?a)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)
[PROOF STEP]
have "[?h = q + q*q + x * y + q - (x * y + (x * q - x*b) + (q - r))] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + x * (q - b) + (q - r))] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + (x * q - x * b) + (q - r))] (mod q)
[PROOF STEP]
by (simp add: right_diff_distrib')
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + (x * q - x * b) + (q - r))] (mod q)

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + (x * q - x * b) + (q - r))] (mod q)
[PROOF STEP]
have "[?h = q + q*q + x * y + q - x * y - (x * q - x*b) - (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - (x * y + (x * q - x * b) + (q - r))] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - x * y - (x * q - x * b) - (q - r)] (mod q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - x * y - (x * q - x * b) - (q - r)] (mod q)

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - x * y - (x * q - x * b) - (q - r)] (mod q)
[PROOF STEP]
have mod': "[?h = q + q*q + q - (x * q - x*b) - (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + x * y + q - x * y - (x * q - x * b) - (q - r)] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - (x * q - x * b) - (q - r)] (mod q)
[PROOF STEP]
by(simp add: add.commute)
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - (x * q - x * b) - (q - r)] (mod q)

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - (x * q - x * b) - (q - r)] (mod q)
[PROOF STEP]
have neg: "[?h = q + q*q + q - x * q +  x*b - (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - (x * q - x * b) - (q - r)] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - (x * q - x * b) - (q - r)] (mod q) \<Longrightarrow> [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
have "[q + q*q + q - (x * q - x*b) - (q - r) = q + q*q + q - x * q + x*b - (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
proof(cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> [q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)
 2. x \<noteq> 0 \<Longrightarrow> [q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> [q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)
 2. x \<noteq> 0 \<Longrightarrow> [q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. [q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> [q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> [q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> [q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
have "x * q - x*b > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x * q - x * b
[PROOF STEP]
using False assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
x < q
a < q
b < q
r < q
y < q

goal (1 subgoal):
 1. 0 < x * q - x * b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < x * q - x * b

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> [q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 < x * q - x * b

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> [q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
have "q + q*q + q - x * q > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < q + q * q + q - x * q
[PROOF STEP]
by (metis assms(1) add.commute diff_mult_distrib2 less_Suc_eq mult.commute mult_Suc_right nat_0_less_mult_iff q_gt_0 zero_less_diff)
[PROOF STATE]
proof (state)
this:
0 < q + q * q + q - x * q

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> [q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < x * q - x * b
0 < q + q * q + q - x * q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < x * q - x * b
0 < q + q * q + q - x * q

goal (1 subgoal):
 1. [q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - (x * q - x * b) - (q - r)] (mod q) \<Longrightarrow> [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
using mod' cong_trans
[PROOF STATE]
proof (prove)
using this:
[q + q * q + q - (x * q - x * b) - (q - r) = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - (x * q - x * b) - (q - r)] (mod q)
\<lbrakk>[?b = ?c] (mod ?a); [?c = ?d] (mod ?a)\<rbrakk> \<Longrightarrow> [?b = ?d] (mod ?a)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - x * q + x * b - (q - r)] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - x * q + x * b - (q - r)] (mod q)

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - x * q + x * b - (q - r)] (mod q)
[PROOF STEP]
have "[?h = q + q*q + q +  x*b - (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - x * q + x * b - (q - r)] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - x * q + x * b - (q - r)] (mod q) \<Longrightarrow> [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
have "[q + q*q + q - x * q +  x*b - (q - r) = q + q*q + q +  x*b - (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
proof(cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> [q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)
 2. x \<noteq> 0 \<Longrightarrow> [q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> [q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)
 2. x \<noteq> 0 \<Longrightarrow> [q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. [q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> [q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> [q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> [q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
have "q*q > x*q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * q < q * q
[PROOF STEP]
using False assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
x < q
a < q
b < q
r < q
y < q

goal (1 subgoal):
 1. x * q < q * q
[PROOF STEP]
by (simp add: mult_strict_mono)
[PROOF STATE]
proof (state)
this:
x * q < q * q

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> [q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x * q < q * q
[PROOF STEP]
have 1: "q + q*q + q - x * q +  x*b - (q - r) > 0"
[PROOF STATE]
proof (prove)
using this:
x * q < q * q

goal (1 subgoal):
 1. 0 < q + q * q + q - x * q + x * b - (q - r)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
0 < q + q * q + q - x * q + x * b - (q - r)

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> [q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < q + q * q + q - x * q + x * b - (q - r)
[PROOF STEP]
have 2: "q + q*q + q +  x*b - (q - r) > 0"
[PROOF STATE]
proof (prove)
using this:
0 < q + q * q + q - x * q + x * b - (q - r)

goal (1 subgoal):
 1. 0 < q + q * q + q + x * b - (q - r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < q + q * q + q + x * b - (q - r)

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> [q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < q + q * q + q + x * b - (q - r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < q + q * q + q + x * b - (q - r)

goal (1 subgoal):
 1. [q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
by (smt 1 2 Nat.add_diff_assoc2 \<open>x * q < q * q\<close> add_cancel_left_left add_diff_inverse_nat
                le_add1 le_add2 le_trans less_imp_add_positive less_numeral_extra(3) minus_mod
                minus_q_mult_cancel mod_if mult.commute q_gt_0)
[PROOF STATE]
proof (state)
this:
[q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - x * q + x * b - (q - r)] (mod q) \<Longrightarrow> [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
using cong_trans neg
[PROOF STATE]
proof (prove)
using this:
[q + q * q + q - x * q + x * b - (q - r) = q + q * q + q + x * b - (q - r)] (mod q)
\<lbrakk>[?b = ?c] (mod ?a); [?c = ?d] (mod ?a)\<rbrakk> \<Longrightarrow> [?b = ?d] (mod ?a)
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q - x * q + x * b - (q - r)] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b - (q - r)] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b - (q - r)] (mod q)

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b - (q - r)] (mod q)
[PROOF STEP]
have "[?h = q + q*q + q +  x*b - q + r] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b - (q - r)] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b - q + r] (mod q)
[PROOF STEP]
by (metis r(1) Nat.add_diff_assoc2 Nat.diff_diff_right le_add2 less_imp_le_nat semiring_normalization_rules(23))
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b - q + r] (mod q)

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b - q + r] (mod q)
[PROOF STEP]
have "[?h = q + q*q + q +  x*b + r] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b - q + r] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b + r] (mod q)
[PROOF STEP]
apply(simp add: cong_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (q * q + (q + x * b) + r) mod q \<Longrightarrow> (q * q + (q + x * b) + r) mod q = (q + q * q + q + x * b + r) mod q
[PROOF STEP]
by (metis (no_types, lifting) add.assoc add.commute add_diff_cancel_right' diff_is_0_eq' mod_if mod_le_divisor q_gt_0)
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b + r] (mod q)

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b + r] (mod q)
[PROOF STEP]
have "[?h = x*b + r] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = q + q * q + q + x * b + r] (mod q)

goal (1 subgoal):
 1. [(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * b + r] (mod q)
[PROOF STEP]
apply(simp add: cong_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (q + q * q + q + x * b + r) mod q \<Longrightarrow> (q + q * q + q + x * b + r) mod q = (x * b + r) mod q
[PROOF STEP]
by (metis mod_add_cong mod_add_self1 mod_mult_self1)
[PROOF STATE]
proof (state)
this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * b + r] (mod q)

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * b + r] (mod q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = x * b + r] (mod q)

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
by (simp add: cong_def assms)
[PROOF STATE]
proof (state)
this:
(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q
[PROOF STEP]
have rhs: "((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x*b + r) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
let ?h = "((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
have "[?h =  (x + a) mod q * b + q - (a * b + (q - r)) mod q] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x + a) mod q * b + q - (a * b + (q - r)) mod q] (mod q)
[PROOF STEP]
by (simp add: q_gt_0  assms(1) cong_def)
[PROOF STATE]
proof (state)
this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x + a) mod q * b + q - (a * b + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x + a) mod q * b + q - (a * b + (q - r)) mod q] (mod q)
[PROOF STEP]
have "[?h = (x + a) * b + q - (a * b + (q - r)) mod q] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x + a) mod q * b + q - (a * b + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x + a) * b + q - (a * b + (q - r)) mod q] (mod q)
[PROOF STEP]
by (smt Nat.add_diff_assoc cong_def mod_add_cong mod_le_divisor mod_mult_left_eq q_gt_0 assms)
[PROOF STATE]
proof (state)
this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x + a) * b + q - (a * b + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x + a) * b + q - (a * b + (q - r)) mod q] (mod q)
[PROOF STEP]
have "[?h = x*b + a*b + q - (a * b + (q - r)) mod q] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x + a) * b + q - (a * b + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = x * b + a * b + q - (a * b + (q - r)) mod q] (mod q)
[PROOF STEP]
by(metis distrib_right)
[PROOF STATE]
proof (state)
this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = x * b + a * b + q - (a * b + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = x * b + a * b + q - (a * b + (q - r)) mod q] (mod q)
[PROOF STEP]
have mod: "[?h = q + x*b + a*b + q - (a * b + (q - r)) mod q] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = x * b + a * b + q - (a * b + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r)) mod q] (mod q)
[PROOF STEP]
by (smt Nat.add_diff_assoc cong_def add.assoc add.commute le_add2 le_trans mod_add_self2 mod_le_divisor q_gt_0)
[PROOF STATE]
proof (state)
this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r)) mod q] (mod q)
[PROOF STEP]
have "[?h =  q + x*b + a*b + q - (a * b + (q - r))] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r)) mod q] (mod q)

goal (1 subgoal):
 1. [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)
[PROOF STEP]
using  q_cong assms(1)
[PROOF STATE]
proof (prove)
using this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r)) mod q] (mod q)
[?a = q + ?a] (mod q)
x < q

goal (1 subgoal):
 1. [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r)) mod q] (mod q); \<And>a. [a = q + a] (mod q); x < q\<rbrakk> \<Longrightarrow> [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)
[PROOF STEP]
have ge: "q + x*b + a*b + q  > (a * b + (q - r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * b + (q - r) < q + x * b + a * b + q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x < q
a < q
b < q
r < q
y < q

goal (1 subgoal):
 1. a * b + (q - r) < q + x * b + a * b + q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a * b + (q - r) < q + x * b + a * b + q

goal (1 subgoal):
 1. \<lbrakk>[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r)) mod q] (mod q); \<And>a. [a = q + a] (mod q); x < q\<rbrakk> \<Longrightarrow> [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a * b + (q - r) < q + x * b + a * b + q
[PROOF STEP]
have "[ q + x*b + a*b + q - (a * b + (q - r)) mod q =  q + x*b + a*b + q - (a * b + (q - r))] (mod q)"
[PROOF STATE]
proof (prove)
using this:
a * b + (q - r) < q + x * b + a * b + q

goal (1 subgoal):
 1. [q + x * b + a * b + q - (a * b + (q - r)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)
[PROOF STEP]
using Divides.mod_less_eq_dividend cong_diff_nat  cong_def le_trans less_not_refl2
                  less_or_eq_imp_le q_gt_0 minus_mod
[PROOF STATE]
proof (prove)
using this:
a * b + (q - r) < q + x * b + a * b + q
(0::?'a) \<le> ?a \<Longrightarrow> ?a mod ?b \<le> ?a
\<lbrakk>[?a = ?b] (mod ?m); [?c = ?d] (mod ?m); ?c \<le> ?a; ?d \<le> ?b\<rbrakk> \<Longrightarrow> [?a - ?c = ?b - ?d] (mod ?m)
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)
\<lbrakk>?i \<le> ?j; ?j \<le> ?k\<rbrakk> \<Longrightarrow> ?i \<le> ?k
?n < ?m \<Longrightarrow> ?m \<noteq> ?n
?m < ?n \<or> ?m = ?n \<Longrightarrow> ?m \<le> ?n
0 < q
?b < ?a \<Longrightarrow> [?a - ?b mod q = ?a - ?b] (mod q)

goal (1 subgoal):
 1. [q + x * b + a * b + q - (a * b + (q - r)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
[q + x * b + a * b + q - (a * b + (q - r)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)

goal (1 subgoal):
 1. \<lbrakk>[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r)) mod q] (mod q); \<And>a. [a = q + a] (mod q); x < q\<rbrakk> \<Longrightarrow> [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[q + x * b + a * b + q - (a * b + (q - r)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[q + x * b + a * b + q - (a * b + (q - r)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)

goal (1 subgoal):
 1. [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)
[PROOF STEP]
using mod cong_trans
[PROOF STATE]
proof (prove)
using this:
[q + x * b + a * b + q - (a * b + (q - r)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r)) mod q] (mod q)
\<lbrakk>[?b = ?c] (mod ?a); [?c = ?d] (mod ?a)\<rbrakk> \<Longrightarrow> [?b = ?d] (mod ?a)

goal (1 subgoal):
 1. [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)

goal (1 subgoal):
 1. ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)
[PROOF STEP]
have "[?h =  q + x*b + q - (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + a * b + q - (a * b + (q - r))] (mod q)

goal (1 subgoal):
 1. [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + q - (q - r)] (mod q)
[PROOF STEP]
by (simp add: add.commute)
[PROOF STATE]
proof (state)
this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + q - (q - r)] (mod q)

goal (1 subgoal):
 1. ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + q - (q - r)] (mod q)
[PROOF STEP]
have "[?h =  q + x*b + q - q + r] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + q - (q - r)] (mod q)

goal (1 subgoal):
 1. [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + q - q + r] (mod q)
[PROOF STEP]
by (metis Nat.add_diff_assoc2 Nat.diff_diff_right r(1) le_add2 less_imp_le_nat)
[PROOF STATE]
proof (state)
this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + q - q + r] (mod q)

goal (1 subgoal):
 1. ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + q - q + r] (mod q)
[PROOF STEP]
have "[?h = q + x*b + r] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + q - q + r] (mod q)

goal (1 subgoal):
 1. [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + r] (mod q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + r] (mod q)

goal (1 subgoal):
 1. ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + r] (mod q)
[PROOF STEP]
have "[?h = q + (x*b + r)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + r] (mod q)

goal (1 subgoal):
 1. [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + (x * b + r)] (mod q)
[PROOF STEP]
using add.assoc
[PROOF STATE]
proof (prove)
using this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + x * b + r] (mod q)
?a + ?b + ?c = ?a + (?b + ?c)

goal (1 subgoal):
 1. [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + (x * b + r)] (mod q)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + (x * b + r)] (mod q)

goal (1 subgoal):
 1. ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + (x * b + r)] (mod q)
[PROOF STEP]
have "[?h = x*b + r] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + (x * b + r)] (mod q)

goal (1 subgoal):
 1. [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = x * b + r] (mod q)
[PROOF STEP]
using cong_def q_cong_reverse
[PROOF STATE]
proof (prove)
using this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = q + (x * b + r)] (mod q)
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)
[q + ?a = ?a] (mod q)

goal (1 subgoal):
 1. [((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = x * b + r] (mod q)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = x * b + r] (mod q)

goal (1 subgoal):
 1. ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = x * b + r] (mod q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = x * b + r] (mod q)

goal (1 subgoal):
 1. ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
by (simp add: cong_def assms(1))
[PROOF STATE]
proof (state)
this:
((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = (x * b + r) mod q
((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * b + r) mod q

goal (1 subgoal):
 1. (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q = ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. ((x + a) mod q * b + q - (a * b + q - r) mod q) mod q = (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q
[PROOF STEP]
have lhs:"((x + a) mod q * b + q - (a * b + q - r) mod q) mod q = ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x + a) mod q * b + q - (a * b + q - r) mod q) mod q = ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x < q
a < q
b < q
r < q
y < q

goal (1 subgoal):
 1. ((x + a) mod q * b + q - (a * b + q - r) mod q) mod q = ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((x + a) mod q * b + q - (a * b + q - r) mod q) mod q = ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. ((x + a) mod q * b + q - (a * b + q - r) mod q) mod q = (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q
[PROOF STEP]
have rhs: "(x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x < q
a < q
b < q
r < q
y < q

goal (1 subgoal):
 1. (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. ((x + a) mod q * b + q - (a * b + q - r) mod q) mod q = (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q
[PROOF STEP]
have " ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q
[PROOF STEP]
using assms s[symmetric]
[PROOF STATE]
proof (prove)
using this:
x < q
a < q
b < q
r < q
y < q
((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. ((x + a) mod q * b + q - (a * b + q - r) mod q) mod q = (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. ((x + a) mod q * b + q - (a * b + q - r) mod q) mod q = (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q
[PROOF STEP]
using lhs rhs
[PROOF STATE]
proof (prove)
using this:
((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q = (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q
((x + a) mod q * b + q - (a * b + q - r) mod q) mod q = ((x + a) mod q * b + (q - (a * b + (q - r)) mod q)) mod q
(x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. ((x + a) mod q * b + q - (a * b + q - r) mod q) mod q = (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
((x + a) mod q * b + q - (a * b + q - r) mod q) mod q = (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma s1_s2_P2:
  assumes "x < q" "xa < q" "xb < q" "xc < q" "y < q"
  shows "((y, xa, (xb * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, ((x + xb) mod q * xa + q - (xb * xa + q - xc) mod q) mod q) =
         ((y, xa, (xb * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((y, xa, (xb * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, ((x + xb) mod q * xa + q - (xb * xa + q - xc) mod q) mod q) = ((y, xa, (xb * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q)
[PROOF STEP]
using assms s1_s2
[PROOF STATE]
proof (prove)
using this:
x < q
xa < q
xb < q
xc < q
y < q
\<lbrakk>?x < q; ?a < q; ?b < q; ?r < q; ?y < q\<rbrakk> \<Longrightarrow> ((?x + ?a) mod q * ?b + q - (?a * ?b + q - ?r) mod q) mod q = (?x * ?y + q - (?x * ((?y + q - ?b) mod q) + q - ?r) mod q) mod q

goal (1 subgoal):
 1. ((y, xa, (xb * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, ((x + xb) mod q * xa + q - (xb * xa + q - xc) mod q) mod q) = ((y, xa, (xb * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q)
[PROOF STEP]
by metis


[STATEMENT]
lemma c1:
  assumes "e2 = (x + c1) mod q"
    and  "x < q" "c1 < q"
  shows "c1 = (e2 + q - x) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c1 = (e2 + q - x) mod q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c1 = (e2 + q - x) mod q
[PROOF STEP]
have "[e2 + q = x + c1] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [e2 + q = x + c1] (mod q)
[PROOF STEP]
by(simp add: assms cong_def)
[PROOF STATE]
proof (state)
this:
[e2 + q = x + c1] (mod q)

goal (1 subgoal):
 1. c1 = (e2 + q - x) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[e2 + q = x + c1] (mod q)
[PROOF STEP]
have "[e2 + q - x  =  c1] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[e2 + q = x + c1] (mod q)

goal (1 subgoal):
 1. [e2 + q - x = c1] (mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [e2 + q = x + c1] (mod q) \<Longrightarrow> [e2 + q - x = c1] (mod q)
[PROOF STEP]
have "e2 + q \<ge> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> e2 + q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
e2 = (x + c1) mod q
x < q
c1 < q

goal (1 subgoal):
 1. x \<le> e2 + q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<le> e2 + q

goal (1 subgoal):
 1. [e2 + q = x + c1] (mod q) \<Longrightarrow> [e2 + q - x = c1] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<le> e2 + q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<le> e2 + q

goal (1 subgoal):
 1. [e2 + q - x = c1] (mod q)
[PROOF STEP]
by (metis \<open>[e2 + q = x + c1] (mod q)\<close> cong_add_lcancel_nat le_add_diff_inverse)
[PROOF STATE]
proof (state)
this:
[e2 + q - x = c1] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[e2 + q - x = c1] (mod q)

goal (1 subgoal):
 1. c1 = (e2 + q - x) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[e2 + q - x = c1] (mod q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[e2 + q - x = c1] (mod q)

goal (1 subgoal):
 1. c1 = (e2 + q - x) mod q
[PROOF STEP]
by(simp add: cong_def assms)
[PROOF STATE]
proof (state)
this:
c1 = (e2 + q - x) mod q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma c1_P2:
  assumes "xb < q" "xa < q" "xc < q" "x < q"
  shows "((y, xa, (xb * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q) =
          ((y, xa, (((x + xb) mod q + q - x) mod q * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((y, xa, (xb * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q) = ((y, xa, (((x + xb) mod q + q - x) mod q * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((y, xa, (xb * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q) = ((y, xa, (((x + xb) mod q + q - x) mod q * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q)
[PROOF STEP]
have "(xb * xa + q - xc) mod q = (((x + xb) mod q + q - x) mod q * xa + q - xc) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xb * xa + q - xc) mod q = (((x + xb) mod q + q - x) mod q * xa + q - xc) mod q
[PROOF STEP]
using assms c1
[PROOF STATE]
proof (prove)
using this:
xb < q
xa < q
xc < q
x < q
\<lbrakk>?e2.0 = (?x + ?c1.0) mod q; ?x < q; ?c1.0 < q\<rbrakk> \<Longrightarrow> ?c1.0 = (?e2.0 + q - ?x) mod q

goal (1 subgoal):
 1. (xb * xa + q - xc) mod q = (((x + xb) mod q + q - x) mod q * xa + q - xc) mod q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(xb * xa + q - xc) mod q = (((x + xb) mod q + q - x) mod q * xa + q - xc) mod q

goal (1 subgoal):
 1. ((y, xa, (xb * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q) = ((y, xa, (((x + xb) mod q + q - x) mod q * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(xb * xa + q - xc) mod q = (((x + xb) mod q + q - x) mod q * xa + q - xc) mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(xb * xa + q - xc) mod q = (((x + xb) mod q + q - x) mod q * xa + q - xc) mod q

goal (1 subgoal):
 1. ((y, xa, (xb * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q) = ((y, xa, (((x + xb) mod q + q - x) mod q * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(xb * xa + q - xc) mod q = (((x + xb) mod q + q - x) mod q * xa + q - xc) mod q
xb < q
xa < q
xc < q
x < q

goal (1 subgoal):
 1. ((y, xa, (xb * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q) = ((y, xa, (((x + xb) mod q + q - x) mod q * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
((y, xa, (xb * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q) = ((y, xa, (((x + xb) mod q + q - x) mod q * xa + q - xc) mod q, (x + xb) mod q), (x * ((y + q - xa) mod q) + q - xc) mod q, (x * y + q - (x * ((y + q - xa) mod q) + q - xc) mod q) mod q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma minus_mod_cancel:
  assumes "a - b > 0" "a - b mod q > 0"
  shows "[a - b + c = a - b mod q + c] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a - b + c = a - b mod q + c] (mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [a - b + c = a - b mod q + c] (mod q)
[PROOF STEP]
have "(b - b mod q + (a - b)) mod q = (0 + (a - b)) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b - b mod q + (a - b)) mod q = (0 + (a - b)) mod q
[PROOF STEP]
using  cong_def mod_add_cong neq0_conv q_gt_0
[PROOF STATE]
proof (prove)
using this:
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)
\<lbrakk>?a mod ?c = ?a' mod ?c; ?b mod ?c = ?b' mod ?c\<rbrakk> \<Longrightarrow> (?a + ?b) mod ?c = (?a' + ?b') mod ?c
(?n \<noteq> 0) = (0 < ?n)
0 < q

goal (1 subgoal):
 1. (b - b mod q + (a - b)) mod q = (0 + (a - b)) mod q
[PROOF STEP]
by (simp add: minus_mod_eq_mult_div)
[PROOF STATE]
proof (state)
this:
(b - b mod q + (a - b)) mod q = (0 + (a - b)) mod q

goal (1 subgoal):
 1. [a - b + c = a - b mod q + c] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(b - b mod q + (a - b)) mod q = (0 + (a - b)) mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(b - b mod q + (a - b)) mod q = (0 + (a - b)) mod q

goal (1 subgoal):
 1. [a - b + c = a - b mod q + c] (mod q)
[PROOF STEP]
by (metis (no_types) Divides.mod_less_eq_dividend Nat.add_diff_assoc2 add_diff_inverse_nat assms(1) cong_def diff_is_0_eq' less_or_eq_imp_le mod_add_cong neq0_conv)
[PROOF STATE]
proof (state)
this:
[a - b + c = a - b mod q + c] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed