fact: Definition mantissa_shrp m d pos := match pos with | pos_Eq => mantissa_shrp_aux m (Z.to_pos d) | _ => pos_Up end.
imports: Coq(ZArith Reals Psatz Bool) Flocq(Zaux Raux) Basic Generic Generic_proof Specific_sig