cleanup

Signed-off-by: Ali Caglayan <[email protected]>

theories/Spaces/Int.v

@@ -8,13 +8,9 @@ Set Cumulativity Weak Constraints.
 
 Declare Scope int_scope.
 
-(** Things that need to go in nat *)
-
-Notation nat_add_assoc := assoc_nat_add.
-
 (** * The Integers *)
 
-(** Definition *)
+(** ** Definition *)
 
 (** We define the integers as two copies of [nat] stuck together. This allows us to reuse many lemmas about arithmetic in nat to prove similar lemmas about integers. *)
 
@@ -92,7 +88,7 @@ Infix "-" := (fun x y => x + -y) : int_scope.
 
 (** *** Multiplication *)
 
-(** We define multiplication of integers by cases on the signs of the integers. *)
+(** We define multiplication of integers by cases on the signs of the integers. Note that in the [negS y, pos x] case the order of the multplication is swapped. This is a trick so that the proof of commutativity becomes easier. *)
 Definition int_mul@{} (x y : Int) : Int :=
   match x, y with
   | pos x, pos y => (x * y)%nat
@@ -361,7 +357,6 @@ Definition int_mul_comm@{} (x y : Int) : x * y = y * x.
 Proof.
   destruct x as [x | x], y as [y | y]; trivial; unfold "*";
     by rewrite nat_mul_comm.
-    Set Printing Universes.
 Defined.
 
 (** Integer multiplication with one on the left is the identity. *)