Prove that succFinitePos and predFinitePos are inverse (#249)
- also merge the zero + denormal branches in ValidFinite - also update some comments - also rearrange some of the existing lemmas
U
Ulf Adams committed
3377662b1958dbdefb679e2c110368512cccf4f6
Parent: 6fbbca4
Committed by GitHub <noreply@github.com>
on 1/10/2026, 12:04:06 PM