Qabs_neg@{} : forall x : Q, abs (- x) = abs x. Proof. intros x. destruct (total_abs_either x) as [[E1 E2]|[E1 E2]]. - rewrite E2. path_via (- - x);[|rewrite involutive;trivial]. apply ((abs_sig (- x)).2). apply flip_nonneg_negate;trivial. - rewrite E2. apply ((abs_sig (- x)).2). apply flip_nonpos_negate;trivial. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.