forall q r : Q, (forall e, close e q r) -> ~ (q < r). Proof. intros q r E1 E2. pose proof (E1 (Qpos_diff _ _ E2)) as E3. apply symmetry in E3;apply Qclose_alt in E3. unfold cast in E3;simpl in E3. apply (irreflexivity lt (r - q)). apply le_lt_trans with (abs (r - q));trivial. apply Qabs_le_raw. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.