constant polynomials

Stream: general

[Jack J Garzella]

I have the following example, which has a proof that seems quite long for the statement:

example {F : Type u} [field F] (a : F) : degree (X - C a) = 1 :=
begin
have deg_X_eq_one : degree (X : polynomial F) = 1,
{ have X_eq_one_mul_X_pow_one : (X : polynomial F) = C 1 * X ^ 1,
  { calc (X : polynomial F) = X ^ 1 : by ring_exp
                      ...   = C 1 * X ^ 1 : by simp },
  rw congr_arg degree X_eq_one_mul_X_pow_one,
  apply @degree_monomial F 1 _ 1 (ne.symm field.zero_ne_one) },
have sub_eq_plus_minus : (X - C a) = (X + C (-a)),
{ simp [map_neg], ring },
rw congr_arg degree sub_eq_plus_minus,
have z_lt_o : (0 : with_bot ℕ) < (1 : with_bot ℕ),
{ have zero_eq_zero_coe : (0 : with_bot ℕ) = ↑(0 : ℕ),
  { by simp },
  have one_eq_one_coe : (1 : with_bot ℕ) = ↑(1 : ℕ),
  { by simp },
  simp [zero_eq_zero_coe, one_eq_one_coe, ←with_bot.some_eq_coe] },
rw (@degree_add_C F (-a) _
                  (X : polynomial F)
                  (by {simp [deg_X_eq_one], exact z_lt_o})),
simp [deg_X_eq_one]
end

Particularly unruly is the part needed to prove that C 1 * X ^ 1 is the same as X, and the part where it takes a bunch of messing with coercions to prove that 0 < 1 remains true in the type with_bot ℕ, as my mathematical brain regards both of those statements as trivial. Any suggestions for shortening/simplifying the proof?

[Chris Hughes]

This is a lemma in the polynomial library degree_X_sub_C. I don't think there's a general nice method for proving these things, it would take me a while to prove this for more complicated polynomials, perhaps a tactic could be written to solve these.