New material added and small changes made.

The only two changes which may affect the behavior of the library in the files compatible with its Nov. 6, 2011 version are as follows:

1. The arguments of the notation "ct" (file hSet.v) have changed. The arguments now are "( R , is , x , y )" where "R" is a relation on an hSet "T",  "is" a proof that "R" is decidable and "x" and "y" are objects of "X" such that "R x y" holds. The previous version required "is" to be a part of a canonical structure on "R" and used Georges Gonthier trick of phantom types.

2. The name of the lemma "plusminusnmm" (file hnat.v) is changed to "minusplusnmm" (since it better confirms with the naming convenion and since another lemma with the name "plusminusnmm" was added).

Other chnages which should not affect the behavior of the library with existing files are as follows:

3. Some changes had to be made in order to ensure that all the files of the library continue working if "total2" is introduced as "Inductive" instead of as "Record". In particular all the uses of canonical structures are removed from the library itself. However, "total2" is still defined through "Record" to make it possible for the users of the library to use canonical structures.

4. A number of simple lemmas were added to hnat.v especially in connection with the behavior of "minus" on natural numbers. This is being done in order to add in a more systematic way some of the results required for the development of the p-adic numbers.