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