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))->(Eq zero m \/ Eq zero n)
one_times_lemma = ... :
{m,n|nat}(Eq one (times m n))->(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)