proposition: Lemma Zabs_5 : forall z p : Z, (Z.abs z <= p)%Z -> (- p <= z <= p)%Z.
proof: Proof. intros. split. replace (- p)%Z with (Z.succ (- Z.succ p)). apply Zlt_le_succ. apply proj2 with (A := (z < Z.succ p)%Z). apply Zabs_1. apply Zle_lt_succ. assumption. unfold Z.succ in |- *. ring. apply Zlt_succ_le. apply proj1 with (B := (- Z.succ p < z)%Z). apply Zabs_1. apply Zle_lt_succ. assumption. Qed.
imports: Coq(Lia)