proposition: Lemma cpoly_mult_cr_c_ : forall p c, (cpoly_mult_cr K p c [=] p [*] _C_ c).
proof: Proof. intros. simpl. induction p. simpl; auto. simpl. split. rewrite cm_rht_unit_unfolded. rewrite mult_commutes. reflexivity. rewrite IHp. reflexivity. Qed.
imports: ssreflect CSetoids CSetoidFun CFields CPolynomials Program Omega Equivalence Morphisms Wf Morphisms CRings CRing_Homomorphisms Rational Setoid CPoly_NthCoeff CPoly_Degree CReals Intervals CauchySeq IntervalFunct MoreIntervals MoreFunctions Composition seq bigopsClass