next up previous contents
Next: The Integers Definitions Up: The Integers Previous: The Integers

Extra lemmas for integers

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_Prop_rels
  weird_thing = ... :
    {x,y,a,b:nat}
    (Eq (plus (times x a) (times y b)) (plus (times x b) (times y a)))->
    (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



Lego
1998-06-15