feat(data/polynomial/monic): add monic_of_mul_monic_left/right (#12446)

Also clean up variables that are defined in the section.

From https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/.60geom_sum.20.28X.20.20n.29.60.20is.20monic/near/274130839

src/data/polynomial/monic.lean

@@ -26,7 +26,7 @@ variables {R : Type u} {S : Type v} {a b : R} {m n : ℕ} {ι : Type y}
 section semiring
 variables [semiring R] {p q r : R[X]}
 
-lemma monic.as_sum {p : R[X]} (hp : p.monic) :
+lemma monic.as_sum (hp : p.monic) :
   p = X^(p.nat_degree) + (∑ i in range p.nat_degree, C (p.coeff i) * X^i) :=
 begin
   conv_lhs { rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm] },
@@ -93,14 +93,28 @@ lemma monic_pow (hp : monic p) : ∀ (n : ℕ), monic (p ^ n)
 | 0     := monic_one
 | (n+1) := by { rw pow_succ, exact monic_mul hp (monic_pow n) }
 
-lemma monic_add_of_left {p q : R[X]} (hp : monic p) (hpq : degree q < degree p) :
+lemma monic_add_of_left (hp : monic p) (hpq : degree q < degree p) :
   monic (p + q) :=
 by rwa [monic, add_comm, leading_coeff_add_of_degree_lt hpq]
 
-lemma monic_add_of_right {p q : R[X]} (hq : monic q) (hpq : degree p < degree q) :
+lemma monic_add_of_right (hq : monic q) (hpq : degree p < degree q) :
   monic (p + q) :=
 by rwa [monic, leading_coeff_add_of_degree_lt hpq]
 
+lemma monic.of_mul_monic_left (hp : p.monic) (hpq : (p * q).monic) : q.monic :=
+begin
+  contrapose! hpq,
+  rw monic.def at hpq ⊢,
+  rwa leading_coeff_monic_mul hp,
+end
+
+lemma monic.of_mul_monic_right (hq : q.monic) (hpq : (p * q).monic) : p.monic :=
+begin
+  contrapose! hpq,
+  rw monic.def at hpq ⊢,
+  rwa leading_coeff_mul_monic hq,
+end
+
 namespace monic
 
 @[simp]