[STATEMENT]
lemma pseudo_mod_zero[simp]:
"pseudo_mod 0 f = (0::'a :: {idom} poly)"
"pseudo_mod f 0 = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pseudo_mod 0 f = 0 &&& pseudo_mod f 0 = f
[PROOF STEP]
unfolding pseudo_mod_def snd_pseudo_mod_smult_left[of 0 _ f,simplified]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = 0 &&& snd (pseudo_divmod f 0) = f
[PROOF STEP]
unfolding pseudo_divmod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = 0 &&& snd (if 0 = 0 then (0, f) else pseudo_divmod_main (lead_coeff 0) 0 f 0 (degree f) (1 + length (coeffs f) - length (coeffs 0))) = f
[PROOF STEP]
by auto