fact: Definition quote_icstr_helper (n : int) : bool * N := match n with | Posz n => (true, N.of_nat n) | Negz n => (false, N.of_nat n) end.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)