fact: Definition Xcmp x y := match x, y with | Xreal u, Xreal v => match Rcompare u v with | Lt => Xlt | Eq => Xeq | Gt => Xgt end | _, _ => Xund end.
imports: Coq(Reals Bool) Flocq(Raux) mathcomp.ssreflect(ssreflect) Stdlib