[STATEMENT]
lemma ab_mod_f0:
  "a = 0 \<or> b = 0" if "a * b mod f = 0" 
    and a: "degree a < degree f" 
    and b: "degree b < degree f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = 0 \<or> b = 0
[PROOF STEP]
using that f_dvd_ab
[PROOF STATE]
proof (prove)
using this:
a * b mod f = 0
degree a < degree f
degree b < degree f
\<lbrakk>f dvd ?a * ?b; degree ?a < degree f; degree ?b < degree f\<rbrakk> \<Longrightarrow> ?a = 0 \<or> ?b = 0

goal (1 subgoal):
 1. a = 0 \<or> b = 0
[PROOF STEP]
by auto