Qabs_nonneg@{} : forall q : Q, 0 <= abs q. Proof. intros q;destruct (total_abs_either q) as [E|E];destruct E as [E1 E2];rewrite E2. - trivial. - apply flip_nonneg_negate. rewrite involutive;trivial. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.