fact: Definition add_slow mode prec (x y : type) := match x, y with | Fnan, _ => x | _, Fnan => y | Float mx ex, Float my ey => match mantissa_sign mx, mantissa_sign my with | Mzero, Mzero => x | Mzero, Mnumber sy py => round_aux mode prec sy py ey pos_Eq | Mnumber sx px, Mzero => round_aux mode prec sx px ex pos_Eq | Mnumber sx px, Mnumber sy py => add_slow_aux2 mode prec sx sy px py ex ey end end.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig