fact: Definition mantissa_shr m d pos := match d with | Zpos nb => iter_pos mantissa_shr_aux nb (m, pos) | _ => (xH, pos_Eq) end.
imports: Coq(ZArith Reals Psatz Bool) Flocq(Zaux Raux) Basic Generic Generic_proof Specific_sig