[STATEMENT]
lemma coprime_inv_hom[simp]: "coprime (Hilbert_Choice.inv hom x') y \<longleftrightarrow> coprime x' (hom y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime (inv hom x') y = coprime x' (hom y)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coprime (inv hom x') y = coprime x' (hom y)
[PROOF STEP]
interpret inv: comm_monoid_mult_isom "Hilbert_Choice.inv hom"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comm_monoid_mult_isom (inv hom)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coprime (inv hom x') y = coprime x' (hom y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime (inv hom x') y = coprime x' (hom y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coprime (inv hom x') y = coprime x' (hom y)

goal:
No subgoals!
[PROOF STEP]
qed