proposition: Lemma monom_S : forall (a : R) n, monom a (S n) [=] _X_[*]monom a n.
proof: Proof. intros. apply eq_transitive_unfolded with (cpoly_linear _ [0] (monom a n)). simpl in |- *. split. algebra. cut (monom a n [=] monom a n). auto. algebra. astepl (_X_[*]monom a n[+]_C_ [0]). Step_final (_X_[*]monom a n[+][0]). Qed.
imports: CoRN.algebra.CPoly_Degree Coq(Lia)