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