x y : int_abs Z N (x * y) = int_abs Z N x * int_abs Z N y. 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.
Require Import