proposition: Lemma abs_mul : forall n m, abs (n * m) == abs n * abs m.
proof: Proof. assert (H : forall n m, 0<=n -> abs (n*m) == n * abs m). { intros n m ?. destruct_max m. - rewrite abs_eq. { apply eq_refl. } now apply mul_nonneg_nonneg. - rewrite abs_neq, mul_opp_r. { reflexivity. } now apply mul_nonneg_nonpos . } intros n m. destruct_max n. - now apply H. - rewrite <- mul_opp_opp, H, abs_opp. { reflexivity. } now apply opp_nonneg_nonpos. Qed.
imports: ZMulOrder