fact: Definition cmp_aux1 m1 m2 := match mantissa_cmp m1 m2 with | Eq => Xeq | Lt => Xlt | Gt => Xgt end.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig