Separated Q. Proof. hnf. intros q r E1. apply tight_apart. intros E2. apply apart_iff_total_lt in E2. destruct E2 as [E2|E2]. - exact (Qclose_separating_not_lt _ _ E1 E2). - refine (Qclose_separating_not_lt _ _ _ E2). intros;symmetry;trivial. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.