proposition: Lemma triangle_IR_minus' : forall x y, AbsIR x[-]AbsIR y [<=] AbsIR (x[-]y).
proof: Proof. intros. eapply leEq_wdr. 2: apply AbsIR_minus. apply shift_minus_leEq; apply shift_leEq_plus'. apply weird_triangleIR. Qed.
imports: CoRN.reals.OddPolyRootIR