proposition: Lemma Zabs_3 : forall z p : Z, (z < p)%Z /\ (- p < z)%Z -> (Z.abs z < p)%Z.
proof: Proof. intros z p. case z. intro. simpl in |- *. elim H. intros. assumption. intros. elim H. intros. simpl in |- *. assumption. intros. elim H. intros. simpl in |- *. apply Zgt_mult_conv_absorb_l with (a := (-1)%Z). constructor. replace (-1 * Zpos p0)%Z with (Zneg p0). replace (-1 * p)%Z with (- p)%Z. apply Z.lt_gt. assumption. ring. simpl in |- *. reflexivity. Qed.
imports: Coq(Lia)