fact: Definition Q_to_approx_decimal_string (x : Q) := if Qeq_bool x 0 then "0.000"%string else if Qle_bool 0 x then positive_rational_to_approx_decimal_string x else append "-" (positive_rational_to_approx_decimal_string (-x)).
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL