proposition: Lemma monom_mult' : forall (a b : R) n, _C_ a[*]monom b n [=] monom (a[*]b) n.
proof: Proof. intros. induction n as [| n Hrecn]. simpl in |- *. split; algebra. astepl (_C_ a[*] (_X_[*]monom b n)). astepl (_C_ a[*]_X_[*]monom b n). astepl (_X_[*]_C_ a[*]monom b n). astepl (_X_[*] (_C_ a[*]monom b n)). Step_final (_X_[*]monom (a[*]b) n). Qed.
imports: CoRN.algebra.CPoly_Degree Coq(Lia)