Qabs_neg_flip@{} : forall a b : Q, abs (a - b) = abs (b - a). Proof. intros a b. rewrite <-Qabs_neg. rewrite <-negate_swap_r. trivial. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.