forall x y : Q, abs x - abs y <= abs (x - y). Proof. intros q r. apply (order_reflecting (+ (abs r))). assert (Hrw : abs q - abs r + abs r = abs q) by ring_tac.ring_with_integers (NatPair.Z nat); rewrite Hrw;clear Hrw. etransitivity;[|apply Q_triangle_le]. assert (Hrw : q - r + r = q) by ring_tac.ring_with_integers (NatPair.Z nat); rewrite Hrw;clear Hrw. reflexivity. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.