fact: Definition z_decode c := match c with |(0%nat, true) => Some 0%Z |(0%nat, false) => None |(n, true) => if (unpickle n) is Some p then Some (Zpos p) else None |(n, false) => if (unpickle n) is Some p then Some (Zneg p) else None end.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith