fact: Definition shl (m : Z) (d : positive) := match m with | Z0 => Z0 | Zpos p => Zpos (shift_pos d p) | Zneg p => Zneg (shift_pos d p) end.
imports: Coq(ZArith Reals Lia) Flocq(Raux Defs Float_prop Operations) Gappa_definitions