[STATEMENT]
lemma dvd_sym_div_mult_right [simp]:
  "(a symdiv b) * b = a" if "b > 0" "b dvd a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a symdiv b * b = a
[PROOF STEP]
using sym_mod_sym_div[of b a] that
[PROOF STATE]
proof (prove)
using this:
0 < b \<Longrightarrow> a symmod b = a - a symdiv b * b
0 < b
b dvd a

goal (1 subgoal):
 1. a symdiv b * b = a
[PROOF STEP]
by simp