For the build a modulo operation lattice, we translate to SMT-Lib2 format
and use the following (name as is from Coq) lemmas: 
mod_pos_bound,
mod_neg_bound, 
Z_mod_remainder, 
Z_mod_lt, 
Zmod_eq_full, 
Zmod_eq, 
Zmod_0_l,
Zmod_0_r, 
Zmod_1_l, 
Zmod_1_r, 
Z_mod_same_full, 
Z_mod_mult, 
Zmod_opp_opp,
Z_mod_zero_opp_full, 
Z_mod_nz_opp_full, 
Z_mod_zero_opp_r, 
Z_mod_nz_opp_r,

and theorems:
Zmod_small, 
Zmod_le, 
Zmod_unique_full, 
Zmod_unique, 
Zmod_mod.

Note: name as is from Coq webpage: