fact: Definition mantissa_shr_aux v := match v with | (xO p, pos_Eq) => (p, pos_Eq) | (xO p, _) => (p, pos_Lo) | (xI p, pos_Eq) => (p, pos_Mi) | (xI p, _) => (p, pos_Up) | _ => (xH, pos_Eq) end.
imports: Coq(ZArith Reals Psatz Bool) Flocq(Zaux Raux) Basic Generic Generic_proof Specific_sig