proposition: Lemma AbsIR_mult_pos : forall x y, [0] [<=] y -> AbsIR (x[*]y) [=] AbsIR x[*]y.
proof: Proof. intros. apply eq_transitive_unfolded with (AbsIR x[*]AbsIR y). apply AbsIR_resp_mult. apply bin_op_wd_unfolded. algebra. unfold AbsIR in |- *; simpl in |- *; unfold ABSIR in |- *. apply eq_transitive_unfolded with (Max [--]y y). apply Max_comm. apply leEq_imp_Max_is_rht. apply leEq_transitive with ZeroR. astepr ( [--]ZeroR). apply inv_resp_leEq; assumption. assumption. Qed.
imports: CoRN.reals.OddPolyRootIR