fact: Definition to_decimal (n : IQ) : option Decimal.decimal := match n with | IQmake num den => IQmake_to_decimal' num den | IQmult (IQmake num den) (IQmake (IZpow_pos 10 e) 1) => match IQmake_to_decimal' num den with | Some (Decimal.Decimal i f) => Some (Decimal.DecimalExp i f (Pos.to_int e)) | _ => None end | IQdiv (IQmake num den) (IQmake (IZpow_pos 10 e) 1) => match IQmake_to_decimal' num den with | Some (Decimal.Decimal i f) => Some (Decimal.DecimalExp i f (Decimal.Neg (Pos.to_uint e))) | _ => None end | _ => None end.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool