fact: Definition build_z_atom_aux a := match a with | Auop UO_Zpos a => option_map Zpos (build_positive a) | Acop CO_Z0 => Some Z0 | Auop UO_Zneg a => option_map Zneg (build_positive a) | _ => None end.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz