take dL-Z_2 ; :: thesis: dL-Z_2 is add-associative
thus dL-Z_2 is add-associative ; :: thesis: verum