This file contains some lemmas about the natural numbers which are needed for developing the integers with this particular representation. These lemmas are needed in order to prove cancellation of multiplication laws in the integers and rationals. For example, the first lemma is the (integer) theorem that if the product of two integers is zero, then one or other of the argument is equal to zero. All these lemmas are proved by a double induction on natural numbers.

** Module lib_int_nat_lemmas Imports lib_nat/lib_nat_Prop_rels weird_thing = ... : {x,y,a,b:nat} (Eq (plus (times x a) (times y b)) (plus (times x b) (times y a)))-> or (Eq x y) (Eq a b) weird_Lt = ... : {x,y,a,b:nat}(Lt x y)->(Lt a b)-> Lt (plus (times x b) (times y a)) (plus (times x a) (times y b)) weird_Le = ... : {x,y,a,b:nat}(Le x y)->(Le a b)-> Le (plus (times x b) (times y a)) (plus (times x a) (times y b)) weird_thing_Le = ... : {x,y,a,b:nat} (Le (plus (times x a) (times y b)) (plus (times x b) (times y a)))-> (Lt x y)->Le b a weird_thing_Lt = ... : {x,y,a,b:nat} (Lt (plus (times x a) (times y b)) (plus (times x b) (times y a)))-> (Lt x y)->Lt b a

Fri May 24 19:01:27 BST 1996