# Total: 20 proofs.

 Barzilay & Lee, 2002 Holland-Minkley et al, 1999 1 (zero_ann_a) Assume that a and b are integers and (a = 0 or b = 0) , we need to show a * b = 0. (a = 0 or b = 0) can be split into two cases a = 0 or not. if a = 0 then a * b = 0. if b = 0 we are done. For an integer a and b, if a = 0 or b = 0 then a * b = 0. Consider that a and b are integers and a = 0 or b = 0. There are 2 possible cases. Now, the goal can be transformed to a * b = 0. Now, the goal can be transformed to a * b = 0. 2 (add_cancel_in_eq) Let a, b and n be integers , a+n = b+n , we need to show a = b. We prove this holds for a+n-n=b+n-n. This case is trivial. For an integer a, b and n, if a+n = b+n then a=b. Consider that a, b and n are integers and a+n = b+n. Equivalently, the original expression can be rewritten as a=b. Equivalently, the goal can be rewritten as (a+n)-n = (b+n)-n. 3 (add_mono_wrt_lt) Assume a, b and n are integers. Show that a < b if and only if a+n < b+n. Using lemma add_cancel_in_lt , we know that the statement is proved. suppose a+n= n, we need to show (a rem n) = ((a-n) rem n). By lemma rem_to_div we show: a-(a/n)*n = a-n-((a-n)/n)*n. By lemma div_rec_case we get : a-(((a-n)/n) 1)*n = a-n-((a-n)/ n)*n. By 0, a + -n + -(n*((a + -n)/n)) = a + -n + -(n*((a + -n)/n)). This case it trivial. For a natural number a and the positive natural number n, if a >= n then a rem n = (a - n) rem n. Assume that a is a natural number, n is the positive natural number and a >= n. By applying the rem_to_div lemma, we know a rem n = (a - n) rem n. From the div_rec_case lemma, we conclude a - (a/n)*n = a - n - ((a - n)/n)*n. Now, the goal can be transformed to a - ((a - n)/n + 1)*n = a - n - ((a - n)/n)*n. Equivalently, the goal can be transformed to a + -n + -(n*((a + -n)/n)) = a + -n + -(n*((a + -n)/n)). 8 (rem_rem_to_rem) Assume that a is a natural number and n is the positive natural number, we need to show ((a rem n) rem n) = (a rem n). By lemma rem_base_case we get the new goal (a rem n) < n and (a rem n) = (a rem n). From the rem_bounds_1 , goal (a rem n) < n follows. Case of (a rem n) = (a rem n) is trivial. For a natural number a and the positive natural number n, (a rem n) rem n = a rem n. Assume that a is a natural number and n is the positive natural number. There are 2 possible cases. By the rem_bounds_1 lemma, we conclude a rem n < n. Equivalently, the goal can be transformed to a rem n = a rem n. 9 (mul_bounds_1b) Let a and b are the positive natural numbers, we need to show 0