`{Abs A} `{!TotalRelation le} : forall x : A, (0 <= x /\ abs x = x) |_| (x <= 0 /\ abs x = - x). Proof. intros x. destruct (total le 0 x) as [E|E]. - left. split;trivial. apply ((abs_sig x).2);trivial. - right. split;trivial. apply ((abs_sig x).2);trivial. Qed.
Require Import HoTT.Classes.interfaces.canonical_names.