How to model an implication

This very simplified form also gives similar results.

julia>  main() do n, N, model, x
                   @variable(model, z, Int)
                   @constraint(model, z == sum(x[1, :]) - N)   
                   @constraint(model, !z --> {sum(x[2, :]) == 2})
               end
Test Summary: | Pass  Total  Time
main          | 4070   4070  0.8s

Is it just a coincidence? Or are the formulations(*) actually equivalent?

(*)I’m having trouble following the logic of the second script.
For example, regarding the statement
@constraint(model, z[3] == z[1] + z[2])

I understand that if z[3]==0 then z[1]==z[2]==0.

I don’t understand how it works in different cases.
For example, if it makes sense, since z is Bin, what happens in the case z[1]==z[2]==1?

Clarabel.jl Apache LP, QP, SOCP, SDP
COSMO.jl Apache LP, QP, SOCP, SDP
DAQP DAQP.jl MIT (Mixed-binary) QP
HiGHS HiGHS.jl MIT (MI)LP, QP
Ipopt Ipopt.jl EPL LP, QP, NLP
MadNLP.jl MIT LP, QP, NLP
NLopt NLopt.jl GPL LP, QP, NLP
OSQP OSQP.jl Apache LP, QP
SCS SCS.jl MIT LP, QP, SOCP, SDP
StatusSwitchingQP.jl MIT LP, QP

These are the ones that deal with quadratic problems.
Which one could I use for my model, with a quadratic objective function?