proposition: Lemma Zabs_9 : forall z p : Z, (0 <= p)%Z -> (p < z)%Z \/ (z < - p)%Z -> (p < Z.abs z)%Z.
proof: Proof. intros. case H0. intro. replace (Z.abs z) with z. assumption. symmetry in |- *. apply Z.abs_eq. apply Zlt_le_weak. apply Z.le_lt_trans with (m := p). assumption. assumption. intro. cut (Z.abs z = (- z)%Z). intro. rewrite H2. apply Zmin_cancel_Zlt. ring_simplify (- - z)%Z. assumption. rewrite Zabs_min. apply Z.abs_eq. apply Zlt_le_weak. apply Z.le_lt_trans with (m := p). assumption. apply Zmin_cancel_Zlt. ring_simplify (- - z)%Z. assumption. Qed.
imports: Coq(Lia)