feat(data/mv_polynomial/basic) induction_on'' (#10621)
A new flavor of `induction_on` which is useful when we do not have ` h_add : ∀p q, M p → M q → M (p + q)` but we have
```
h_add_weak : ∀ (a : σ →₀ ℕ) (b : R) (f : (σ →₀ ℕ) →₀ R), a ∉ f.support → b ≠ 0 → M f → M (monomial a b + f)
```
Co-authored-by: Iván Sadofschi Costa <isadofschi@users.noreply.github.com>
