fact: Definition float_array_max a := float_array_max_partial a (Uint63.to_Z (PArray.length a)).
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)