let a, b, k be Nat; :: thesis: ( k < a implies ((a * b) + k) mod a = k )
assume k < a ; :: thesis: ((a * b) + k) mod a = k
hence k = k mod a by NAT_D:24
.= ((a * b) + k) mod a by NAT_D:21 ;
:: thesis: verum