In this file are theorems about multiplication, including those also involving addition e.g. the distributivity laws.

** Module lib_nat_times_thms Imports lib_nat_plus_thms times_plus_dist_r = ... : {i,j,k|nat}Eq (times (plus i j) k) (plus (times i k) (times j k)) times_plus_dist_l = ... : {i,j,k|nat}Eq (times i (plus j k)) (plus (times i j) (times i k)) times_assoc = ... : {i,j,k|nat}Eq (times (times i j) k) (times i (times j k)) times_zero = ... : {n|nat}Eq zero (times n zero) times_one = ... : {n|nat}Eq n (times one n) zero_times_lemma = ... : {m,n|nat}(Eq zero (times m n))->or (Eq zero m) (Eq zero n) one_times_lemma = ... : {m,n|nat}(Eq one (times m n))->and (Eq one m) (Eq one n) times_commutes = ... : {m,n|nat}Eq (times m n) (times n m) times_cancel_right = ... : {a,x,y:nat}(Eq (times x (suc a)) (times y (suc a)))->Eq x y times_two = ... : {n:nat}Eq (times two n) (plus n n)

Fri May 24 19:01:27 BST 1996