[STATEMENT]
lemma radical_dvd [simp, intro]: "radical x dvd x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. radical x dvd x
[PROOF STEP]
by (cases "x = 0") (force intro: prime_factorization_subset_imp_dvd mset_set_set_mset_msubset)+