proposition: Lemma int_abs_negate x : int_abs Z N (-x) = int_abs Z N x.
proof: Proof. destruct (int_abs_spec x) as [[_ E]|[_ E]]. - path_via (int_abs Z N (- f (int_abs Z N x))). apply int_abs_negate_nat. - rewrite <-E. apply int_abs_nat. Qed.
imports: HoTT.Classes.interfaces.naturals HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.nat_int HoTT.Classes.theory.integers HoTT.Classes.theory.rings HoTT.Classes.theory.groups HoTT.Classes.orders.rings