fact: Definition Z_to_string (z : Z) := if (z =? 0)%Z then "0"%string else if (z <? 0)%Z then append "-" (positive_Z_to_decimal_string (S (Z.abs_nat (Z.log2_up (- z)))) (- z)) else (positive_Z_to_decimal_string (S (Z.abs_nat (Z.log2_up z))) z).
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL