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)