proposition: Lemma Zabs_plus : forall z p : Z, (Z.abs (z + p) <= Z.abs z + Z.abs p)%Z.
proof: Proof. intros. case z. simpl in |- *. apply Z.le_refl. case p. intro. simpl in |- *. apply Z.le_refl. intros. simpl in |- *. apply Z.le_refl. intros. unfold Z.abs at 2 in |- *. unfold Z.abs at 2 in |- *. apply Zabs_8. split. apply Zplus_le_reg_l with (Zpos p1 - Zneg p0)%Z. replace (Zpos p1 - Zneg p0 + - (Zpos p1 + Zpos p0))%Z with (- (Zpos p0 + Zneg p0))%Z. replace (Zpos p1 - Zneg p0 + (Zpos p1 + Zneg p0))%Z with (2 * Zpos p1)%Z. replace (- (Zpos p0 + Zneg p0))%Z with 0%Z. apply Zmult_gt_0_le_0_compat. constructor. apply Zlt_le_weak. constructor. rewrite <- Zopp_neg with p0. ring. ring. ring. apply Zplus_le_compat. apply Z.le_refl. apply Zlt_le_weak. constructor. case p. simpl in |- *. intro. apply Z.le_refl. intros. unfold Z.abs at 2 in |- *. unfold Z.abs at 2 in |- *. apply Zabs_8. split. apply Zplus_le_reg_l with (Zpos p1 + Zneg p0)%Z. replace (Zpos p1 + Zneg p0 + - (Zpos p1 + Zpos p0))%Z with (Zneg p0 - Zpos p0)%Z. replace (Zpos p1 + Zneg p0 + (Zneg p1 + Zpos p0))%Z with 0%Z. apply Zplus_le_reg_l with (Zpos p0). replace (Zpos p0 + (Zneg p0 - Zpos p0))%Z with (Zneg p0). simpl in |- *. apply Zlt_le_weak. constructor. ring. replace (Zpos p1 + Zneg p0 + (Zneg p1 + Zpos p0))%Z with (Zpos p1 + Zneg p1 + (Zpos p0 + Zneg p0))%Z. replace 0%Z with (0 + 0)%Z. apply Zplus_eq_compat. rewrite <- Zopp_neg with p1. ring. rewrite <- Zopp_neg with p0. ring. simpl in |- *. constructor. ring. ring. apply Zplus_le_compat. apply Zlt_le_weak. constructor. apply Z.le_refl. intros. simpl in |- *. apply Z.le_refl. Qed.
imports: Coq(Lia)