proposition: Lemma monom_mult : forall (a b : R) m n, monom a m[*]monom b n [=] monom (a[*]b) (m + n).
proof: Proof. intros. induction m as [| m Hrecm]; intros. replace (monom a 0) with (_C_ a). algebra. algebra. astepl (_X_[*]monom a m[*]monom b n). astepl (_X_[*] (monom a m[*]monom b n)). replace (S m + n) with (S (m + n)). Step_final (_X_[*]monom (a[*]b) (m + n)). auto. Qed.
imports: CoRN.algebra.CPoly_Degree Coq(Lia)