In this file are given some basic definitions for the integers. The datatype itself, its equality, various constants and some operations are defined. The internal sigma-type is used to define the pairs of integers. This is mainly because using inductive cross-product is slower to run.
** Module lib_int_basics Imports lib_int_nat_lemmas lib_nat_minus_thms lib_sets_ccmj zed = ... : Type Eq_zed = ... : zed->zed->Prop Eq_refl_zed = ... : refl Eq_zed Eq_sym_zed = ... : sym Eq_zed Eq_trans_zed = ... : trans Eq_zed int = ... : set zero_zed = ... : int.1 one_zed = ... : int.1 two_zed = ... : int.1 three_zed = ... : int.1 four_zed = ... : int.1 minus_one_zed = ... : int.1 plus_zed = ... : int.1->int.1->int.1 times_zed = ... : int.1->int.1->int.1 minus_zed = ... : int.1->int.1->int.1 neg_zed = ... : int.1->int.1