Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama: Quotient Module of Z-module. Formaliz. Math. 20(3): 205-214 (2012)