let a be Nat; :: thesis: for b, c being non zero Nat holds (a mod c) + (b mod c) >= (a + b) mod c
let b, c be non zero Nat; :: thesis: (a mod c) + (b mod c) >= (a + b) mod c
((a mod c) + (b mod c)) mod c <= (a mod c) + (b mod c) by AMB;
hence (a mod c) + (b mod c) >= (a + b) mod c by NAT_D:66; :: thesis: verum