fact: Definition add_slow_aux1 mode prec sx sy mx my e := if eqb sx sy then round_aux mode prec sx (mantissa_add mx my) e pos_Eq else match mantissa_cmp mx my with | Eq => zero | Gt => round_aux mode prec sx (mantissa_sub mx my) e pos_Eq | Lt => round_aux mode prec sy (mantissa_sub my mx) e pos_Eq end.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig