proposition: Theorem Zlt_Zabs_inv1 : forall z1 z2 : Z, (Z.abs z1 < z2)%Z -> (- z2 < z1)%Z.
proof: Proof. intros z1 z2 H; case (Zle_or_lt 0 z1); intros H1. apply Z.lt_le_trans with (- (0))%Z; lia. rewrite <- (Z.opp_involutive z1); rewrite <- (Zabs_eq_opp z1); auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz