fact: Definition Fcmp {beta} (f1 f2 : float beta) := match f1, f2 with | Fnan, _ => Xund | _, Fnan => Xund | Fzero, Fzero => Xeq | Fzero, Float false _ _ => Xlt | Fzero, Float true _ _ => Xgt | Float false _ _, Fzero => Xgt | Float true _ _, Fzero => Xlt | Float false _ _, Float true _ _ => Xgt | Float true _ _, Float false _ _ => Xlt | Float false m1 e1, Float false m2 e2 => Fcmp_aux2 beta m1 e1 m2 e2 | Float true m1 e1, Float true m2 e2 => Fcmp_aux2 beta m2 e2 m1 e1 end.
imports: Coq(Reals Bool ZArith) Flocq(Zaux Raux Div Sqrt) Xreal Basic