fact: Definition z_code (z : Z) := match z with |0%Z => (0%nat, true) |Zpos p => (pickle p, true) |Zneg p => (pickle p, false) end.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith