[STATEMENT]
lemma degree_le_max_perm_degree: "degree (det A) \<le> max_perm_degree A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (Square_Matrix.det A) \<le> max_perm_degree A
[PROOF STEP]
unfolding det_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (\<Sum>p | p permutes UNIV. of_int (sign p) * (\<Prod>i\<in>UNIV. to_fun A i (p i))) \<le> max_perm_degree A
[PROOF STEP]
by (rule order_trans[OF degree_sum_le_Max])
     (auto intro!: degree_prod_le_max_perm_degree Max_le_iff[THEN iffD2] permutes_id simp: sign_permut)