[STATEMENT]
lemma irreducible\<^sub>d_mI:
  assumes f0: "degree_m f > 0"
      and main: "\<And>g h. Mp g = g \<Longrightarrow> Mp h = h \<Longrightarrow> degree g > 0 \<Longrightarrow> degree g < degree_m f \<Longrightarrow> degree h > 0 \<Longrightarrow> degree h < degree_m f \<Longrightarrow> f =m g * h \<Longrightarrow> False"
    shows "irreducible\<^sub>d_m f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreducible\<^sub>d_m f
[PROOF STEP]
proof (unfold irreducible\<^sub>d_m_def, intro conjI allI impI f0 notI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g h. \<lbrakk>degree_m g < degree_m f; degree_m h < degree_m f; f =m g * h\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix g h
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g h. \<lbrakk>degree_m g < degree_m f; degree_m h < degree_m f; f =m g * h\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume deg: "degree_m g < degree_m f" "degree_m h < degree_m f" and "f =m g * h"
[PROOF STATE]
proof (state)
this:
degree_m g < degree_m f
degree_m h < degree_m f
f =m g * h

goal (1 subgoal):
 1. \<And>g h. \<lbrakk>degree_m g < degree_m f; degree_m h < degree_m f; f =m g * h\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
degree_m g < degree_m f
degree_m h < degree_m f
f =m g * h
[PROOF STEP]
have f: "f =m Mp g * Mp h"
[PROOF STATE]
proof (prove)
using this:
degree_m g < degree_m f
degree_m h < degree_m f
f =m g * h

goal (1 subgoal):
 1. f =m Mp g * Mp h
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f =m Mp g * Mp h

goal (1 subgoal):
 1. \<And>g h. \<lbrakk>degree_m g < degree_m f; degree_m h < degree_m f; f =m g * h\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "degree_m f \<le> degree_m g + degree_m h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree_m f \<le> degree_m g + degree_m h
[PROOF STEP]
unfolding f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree_m (Mp g * Mp h) \<le> degree_m g + degree_m h
[PROOF STEP]
using degree_mult_le order.trans
[PROOF STATE]
proof (prove)
using this:
degree (?p * ?q) \<le> degree ?p + degree ?q
\<lbrakk>?a \<le> ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a \<le> ?c

goal (1 subgoal):
 1. degree_m (Mp g * Mp h) \<le> degree_m g + degree_m h
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
degree_m f \<le> degree_m g + degree_m h

goal (1 subgoal):
 1. \<And>g h. \<lbrakk>degree_m g < degree_m f; degree_m h < degree_m f; f =m g * h\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with main[of "Mp g" "Mp h"] deg f
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Mp g =m g; Mp h =m h; 0 < degree_m g; degree_m g < degree_m f; 0 < degree_m h; degree_m h < degree_m f; f =m Mp g * Mp h\<rbrakk> \<Longrightarrow> False
degree_m g < degree_m f
degree_m h < degree_m f
f =m Mp g * Mp h
degree_m f \<le> degree_m g + degree_m h
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Mp g =m g; Mp h =m h; 0 < degree_m g; degree_m g < degree_m f; 0 < degree_m h; degree_m h < degree_m f; f =m Mp g * Mp h\<rbrakk> \<Longrightarrow> False
degree_m g < degree_m f
degree_m h < degree_m f
f =m Mp g * Mp h
degree_m f \<le> degree_m g + degree_m h

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed