proposition: Lemma AbsIR_mult_pos' : forall x y, [0] [<=] x -> AbsIR (x[*]y) [=] x[*]AbsIR y.
proof: Proof. intros. astepl (AbsIR (y[*]x)). eapply eq_transitive_unfolded. apply AbsIR_mult_pos; auto. algebra. Qed.
imports: CoRN.reals.OddPolyRootIR