let l, m, n be Nat; :: thesis: (l + m) mod n = ((l mod n) + (m mod n)) mod n
thus (l + m) mod n = ((l mod n) + m) mod n by NAT_D:22
.= ((l mod n) + (m mod n)) mod n by NAT_D:23 ; :: thesis: verum