Less equal on partially ordered set is reflexive

And fix some typos

MIL/C06_Structures/S02_Algebraic_Structures.lean

@@ -14,7 +14,7 @@ it will help to consider some examples.
 
 #. A *partially ordered set* consists of a set :math:`P` and
    a binary relation :math:`\le` on :math:`P` that is transitive
-   and antireflexive.
+   and reflexive.
 
 #. A *group* consists of a set :math:`G` with an associative
    binary operation, an identity element

MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean

@@ -302,7 +302,7 @@ numbers, carry out the division
 
 The real and imaginary parts might not be integers, but we can round
 them to the nearest integers :math:`u` and :math:`v`. We can then express the
-right-hand size as :math:`(u + vi) + (u' + v'i)`, where
+right-hand side as :math:`(u + vi) + (u' + v'i)`, where
 :math:`u' + v'i` is the part left over. Note that we have
 :math:`|u'| \le 1/2` and :math:`|v'| \le 1/2`, and hence
 
@@ -538,7 +538,7 @@ We just defined the real and imaginary parts of ``x / y`` to be
 respectively.
 Calculating, we have
 
-  ``(x % y) * conj y = (x - x / y * y) * conj y = x * conj y - x * (y * conj j)``
+  ``(x % y) * conj y = (x - x / y * y) * conj y = x * conj y - x / y * (y * conj y)``
 
 The real and imaginary parts of the right-hand side are exactly ``mod' (x * conj y).re (norm y)`` and ``mod' (x * conj y).im (norm y)``.
 By the properties of ``div'`` and ``mod'``,