proposition: Lemma int_abs_mult x y : int_abs Z N (x * y) = int_abs Z N x * int_abs Z N y.
proof: Proof. apply (injective f). rewrite (preserves_mult (f:=f)). destruct (int_abs_spec x) as [[? Ex]|[? Ex]], (int_abs_spec y) as [[? Ey]|[? Ey]]; rewrite Ex, Ey. - rewrite int_abs_nonneg;trivial. apply nonneg_mult_compat;trivial. - rewrite int_abs_nonpos. + apply negate_mult_distr_r. + apply nonneg_nonpos_mult;trivial. - rewrite int_abs_nonpos. + apply negate_mult_distr_l. + apply nonpos_nonneg_mult;trivial. - rewrite int_abs_nonneg. + symmetry;apply negate_mult_negate. + apply nonpos_mult;trivial. 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