Comment by keel-control

there is a proof in lean4 it's correct by construction