fact: Definition shr_aux (p : rnd_record) : rnd_record := let s := rnd_r p || rnd_s p in match (rnd_m p) with | N0 => rnd_record_mk N0 false s | Npos m1 => match m1 with | xH => rnd_record_mk N0 true s | xO m2 => rnd_record_mk (Npos m2) false s | xI m2 => rnd_record_mk (Npos m2) true s end end.
imports: Coq(Decidable Bool ZArith Reals Lia) Flocq(Core Bracket Digits) Gappa_definitions Gappa_dyadic Gappa_round_def Gappa_round_aux