fact: Definition z_unpickle n := match (unpickle n) with |None => None |Some u => z_decode u end.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith