proposition: Lemma abs_triangle : forall n m, abs (n + m) <= abs n + abs m.
proof: Proof. intros n m. destruct_max n; destruct_max m. - rewrite abs_eq. { apply le_refl. } now apply add_nonneg_nonneg. - destruct_max (n+m); try rewrite opp_add_distr; apply add_le_mono_l || apply add_le_mono_r. + apply le_trans with 0; auto. now rewrite opp_nonneg_nonpos. + apply le_trans with 0; auto. now rewrite opp_nonpos_nonneg. - destruct_max (n+m); try rewrite opp_add_distr; apply add_le_mono_l || apply add_le_mono_r. + apply le_trans with 0; auto. now rewrite opp_nonneg_nonpos. + apply le_trans with 0; auto. now rewrite opp_nonpos_nonneg. - rewrite abs_neq, opp_add_distr. { apply le_refl. } now apply add_nonpos_nonpos. Qed.
imports: ZMulOrder