pub proof fn lemma_mod_0_add(a: int, b: int, m: int)Expand description
requires
0 < m,a % m == 0,b % m == 0,(a + b) % m == 0,pub proof fn lemma_mod_0_add(a: int, b: int, m: int)0 < m,a % m == 0,b % m == 0,(a + b) % m == 0,