fact: Fixpoint mantissa_shrp_aux m d := match m with | xO m1 => if (d =? 1)%positive then pos_Up else mantissa_shrp_aux m1 (Pos.pred d) | xI m1 => pos_Up | xH => if (d =? 1)%positive then pos_Mi else pos_Up end.
imports: Coq(ZArith Reals Psatz Bool) Flocq(Zaux Raux) Basic Generic Generic_proof Specific_sig