Qabs_le_raw@{} : forall x : Q, x <= abs x. Proof. intros x;destruct (total_abs_either x) as [[E1 E2]|[E1 E2]]. - rewrite E2;reflexivity. - transitivity (0:Q);trivial. rewrite E2. apply flip_nonpos_negate. trivial. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.