fact: Definition div_aux mode prec s mx my e := let (q, pos) := mantissa_div mx my in round_aux mode prec s q e pos.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig