proposition: Lemma total_abs_either `{Abs A} `{!TotalRelation le} : forall x : A, (0 <= x /\ abs x = x) |_| (x <= 0 /\ abs x = - x).
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra