proposition: Lemma AbsIR_nexp : forall x n, AbsIR (nexp _ n x) [=] nexp _ n (AbsIR x).
proof: Proof. intros. induction n as [| n Hrecn]. simpl in |- *; apply AbsIR_eq_x; apply less_leEq; apply pos_one. simpl in |- *. eapply eq_transitive_unfolded. apply AbsIR_resp_mult. algebra. Qed.
imports: CoRN.reals.OddPolyRootIR