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