let a be Nat; :: thesis: for t, u being Integer holds (- t) mod a = ((u * a) - (t mod a)) mod a
let t, u be Integer; :: thesis: (- t) mod a = ((u * a) - (t mod a)) mod a
thus ((u * a) - (t mod a)) mod a = (((0 + (u * a)) mod a) - ((t mod a) mod a)) mod a by INT_6:7
.= ((0 mod a) - (t mod a)) mod a
.= (0 - t) mod a by INT_6:7
.= (- t) mod a ; :: thesis: verum