proposition: Lemma triangle_IR_minus : forall x y, AbsIR (x[-]y) [<=] AbsIR x[+]AbsIR y.
proof: Proof. intros. unfold cg_minus in |- *. apply leEq_wdr with (AbsIR x[+]AbsIR [--]y). apply triangle_IR. apply bin_op_wd_unfolded. algebra. unfold AbsIR in |- *; simpl in |- *; unfold ABSIR in |- *. apply eq_transitive_unfolded with (Max [--]y y). apply bin_op_wd_unfolded; algebra. apply Max_comm. Qed.
imports: CoRN.reals.OddPolyRootIR