fact: Definition min x y := match cmp x y with | Xlt => x | Xeq => x | Xgt => y | Xund => nan end.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig