Theorems about roundUp and roundDown.

theorem Dyadic.roundDown_le {x : Dyadic} {prec : Int} : x.roundDown prec ≤ x

theorem Dyadic.precision_roundDown {x : Dyadic} {prec : Int} : (x.roundDown prec).precision ≤ some prec

theorem Dyadic.le_roundUp {x : Dyadic} {prec : Int} : x ≤ x.roundUp prec

theorem Dyadic.precision_roundUp {x : Dyadic} {prec : Int} : (x.roundUp prec).precision ≤ some prec