proposition: Lemma Zabs_1 : 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. split. assumption. apply Zgt_mult_conv_absorb_l with (a := (-1)%Z). replace (-1)%Z with (Z.pred 0). apply Zlt_pred. simpl; trivial. ring_simplify (-1 * - p)%Z (-1 * 0)%Z. apply Z.lt_gt. assumption. intros. simpl in H. split. assumption. apply Z.lt_trans with (m := 0%Z). apply Zgt_mult_conv_absorb_l with (a := (-1)%Z). replace (-1)%Z with (Z.pred 0). apply Zlt_pred. simpl; trivial. ring_simplify (-1 * - p)%Z (-1 * 0)%Z. apply Z.lt_gt. apply Z.lt_trans with (m := Zpos p0). constructor. assumption. constructor. intros. simpl in H. split. apply Z.lt_trans with (m := Zpos p0). constructor. assumption. apply Zgt_mult_conv_absorb_l with (a := (-1)%Z). replace (-1)%Z with (Z.pred 0). apply Zlt_pred. simpl;trivial. ring_simplify (-1 * - p)%Z. replace (-1 * Zneg p0)%Z with (- Zneg p0)%Z. replace (- Zneg p0)%Z with (Zpos p0). apply Z.lt_gt. assumption. symmetry in |- *. apply Zopp_neg. rewrite Zopp_mult_distr_l_reverse with (n := 1%Z). simpl in |- *. constructor. Qed.
imports: Coq(Lia)