proposition: Lemma AbsIR_less_square : forall x y, AbsIR x [<] y -> x[^]2 [<] y[^]2.
proof: Proof. intros. eapply less_wdl. 2: apply AbsIR_eq_x; apply sqr_nonneg. eapply less_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_nexp_op. apply nexp_resp_less; auto. apply AbsIR_nonneg. Qed.
imports: CoRN.reals.OddPolyRootIR