`max` and `min`

[quinn-dougherty]

One way I'd do this is adding a subdir at the top

$ ls FlocqExtern/IEEE754
BinarySingleNan.v Binary.v

and try to spoof the patterns in Flocq.IEEE754.Binary{SingleNaN,}.v

Once Bmax is vendored that way (and coq_makefile/_CoqProject are caught up), follow the patterns in IEEE754_extras.v appending Bmax and proofs.

Would yall have a preferred design @ak-2485 @andrew-appel ? or does this sound reasonable?