Qabs_nonpos_0@{} : forall q : Q, abs q <= 0 -> q = 0. Proof. intros q E. pose proof (antisymmetry le _ _ E (Qabs_nonneg _)) as E1. destruct (total_abs_either q) as [[E2 E3]|[E2 E3]];rewrite E3 in E1. - trivial. - apply (injective (-)). rewrite negate_0. trivial. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.