proposition: Lemma Zabs_4 : forall z p : Z, (Z.abs z < p)%Z -> (- p < z < p)%Z.
proof: Proof. intros. split. apply proj2 with (A := (z < p)%Z). apply Zabs_1. assumption. apply proj1 with (B := (- p < z)%Z). apply Zabs_1. assumption. Qed.
imports: Coq(Lia)