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: