Qclose_neg@{} : forall e (x y : Q), close e x y <-> close e (- x) (- y). Proof. intros e x y;split;intros E;apply Qclose_alt in E;apply Qclose_alt. - rewrite <-(negate_plus_distr),Qabs_neg. trivial. - rewrite <-(negate_plus_distr),Qabs_neg in E. trivial. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.