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