This file contains some basic theorems about the integers involving the algebraic operators, e.g. commutativity, associativity etc. Note this file takes quite a long time to load.
The variable eq is a generic equality for any set and is defined in the file in the directory lib_sets. Here it is always implicitly specialised to Eq_zed which is the equality defined on the set int in the file lib_int_basics.
** Module lib_int_basics_thms Imports lib_int_basics times_one_zed = ... : {m|int.1}eq m (times_zed one_zed m) middle_four_plus_zed = ... : {a,b,c,d|int.1} eq (plus_zed (plus_zed a c) (plus_zed b d)) (plus_zed (plus_zed a b) (plus_zed c d)) times_plus_dist_r_zed = ... : {a,b,c|int.1} eq (times_zed (plus_zed a b) c) (plus_zed (times_zed a c) (times_zed b c)) times_plus_dist_l_zed = ... : {a,b,c|int.1} eq (times_zed c (plus_zed a b)) (plus_zed (times_zed c a) (times_zed c b)) times_resp_eq_l = ... : {a,b,x:int.1}(eq a b)->eq (times_zed x a) (times_zed x b) plus_commutes_zed = ... : {p,q|int.1}Eq (plus_zed p q) (plus_zed q p) times_commutes_zed = ... : {p,q|int.1}Eq (times_zed p q) (times_zed q p) times_assoc_zed = ... : {a,b,c|int.1} eq (times_zed (times_zed a b) c) (times_zed a (times_zed b c)) plus_resp_eq = ... : {a,b,x,y:int.1}(eq a b)->(eq x y)->eq (plus_zed a x) (plus_zed b y) minus_resp_eq = ... : {a,b,x,y:int.1}(eq a b)->(eq x y)-> eq (minus_zed a x) (minus_zed b y) times_resp_eq_r = ... : {a,b,x:int.1}(eq a b)->eq (times_zed a x) (times_zed b x) times_resp_eq = ... : {a,b,x,y:int.1}(eq a b)->(eq x y)-> eq (times_zed a x) (times_zed b y) neg_resp_eq = ... : {x,y:int.1}(eq x y)->eq (neg_zed x) (neg_zed y) neg_minus = ... : {x,y:int.1}eq (plus_zed x (neg_zed y)) (minus_zed x y) times_cancel_left_zed = ... : {x,y,a:int.1}(not (eq a zero_zed))-> (eq (times_zed a x) (times_zed a y))->eq x y middle_four_times_zed = ... : {x,y,a,b:int.1} eq (times_zed (times_zed x y) (times_zed a b)) (times_zed (times_zed x a) (times_zed y b)) eq_zero_zed_imp = ... : {x:zed}(eq zero_zed x)->Eq x.1 x.2 imp_eq_zero_zed = ... : {x:zed}(Eq x.1 x.2)->eq zero_zed x times_zero_lemma_zed = ... : {x,y:zed}(eq (times_zed x y) zero_zed)-> (eq zero_zed x \/ eq zero_zed y) right_dist_minus_times_zed = ... : {a,b,c|int.1} eq (times_zed (minus_zed a b) c) (minus_zed (times_zed a c) (times_zed b c)) times_neg = ... : {x,y:int.1}eq (times_zed x (neg_zed y)) (times_zed y (neg_zed x)) times_neg_both = ... : {x,y:int.1}eq (times_zed x y) (times_zed (neg_zed x) (neg_zed y)) plus_assoc_zed = ... : {a,b,c|int.1} eq (plus_zed (plus_zed a b) c) (plus_zed a (plus_zed b c)) one_times_zed = ... : {x:int.1}eq (times_zed one_zed x) x plus_zero_zed = ... : {x:int.1}eq (plus_zed x zero_zed) x minus_zed_is = ... : {x,y,z:int.1}iff (eq (minus_zed x y) z) (eq x (plus_zed y z)) n_minus_n_Eq_zero_zed = ... : {x:int.1}eq (minus_zed x x) zero_zed plus_inv_minus_zed = ... : {x,y:int.1}eq (plus_zed (minus_zed x y) y) x bring_neg_out = ... : {x,y:int.1}eq (times_zed (neg_zed x) y) (neg_zed (times_zed x y)) minus_is_minus_zed = ... : {a,b:nat}(Le a b)->eq (minus_zed (b,zero) (a,zero)) (minus b a,zero)