fact: Definition rounding_mode_of_mode md := match md with | mode_NE | mode_NA => Basic.rnd_NE | mode_ZR => Basic.rnd_ZR | mode_DN => Basic.rnd_DN | mode_UP => Basic.rnd_UP end.
imports: Coq(Bool Floats Reals List Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations) Specific_bigint Specific_ops Interval_helper Float_full Prog Lang_expr