∀ {R : Type u_1} [inst : Semiring R] [inst_1 : MulSemiringAction (Multiplicative ℕ) R] (n m : ℕ) (r s : R),
  (SkewPolynomial.monomial n) r * (SkewPolynomial.monomial m) s =
    (SkewPolynomial.monomial (n + m)) (r * (⇑SkewPolynomial.φ)^[n] s)