forall q : Q, q = 0 |_| 0 < abs q. Proof. intros q. destruct (le_or_lt (abs q) 0) as [E|E]. - left. apply Qabs_nonpos_0. trivial. - right. trivial. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.