fact: Definition float_array_min_partial a i := snd (N.iter (Z.to_N i) (fun '(n, x) => (Z.succ n, float_min x (PArray.get a (Uint63.of_Z n)))) (0%Z, infinity)).
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)