doc(data/nat/modeq): add module docstring and lemma (#2528)

I add a simple docstrong and also a lemma which I found useful for a codewars kata.

Author: kbuzzard

src/data/nat/modeq.lean

@@ -2,13 +2,25 @@
 Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
-
-Modular equality relation.
 -/
 import data.int.gcd
 import tactic.abel
 import data.list.rotate
+/-
+# Congruences modulo a natural number
+
+This file defines the equivalence relation `a ≡ b [MOD n]` on the natural numbers,
+and proves basic properties about it such as the Chinese Remainder Theorem
+`modeq_and_modeq_iff_modeq_mul`.
+
+## Notations
 
+`a ≡ b [MOD n]` is notation for `modeq n a b`, which is defined to mean `a % n = b % n`.
+
+## Tags
+
+modeq, congruence, mod, MOD, modulo
+-/
 namespace nat
 
 /-- Modular equality. `modeq n a b`, or `a ≡ b [MOD n]`, means
@@ -37,6 +49,10 @@ by rw [modeq, eq_comm, ← int.coe_nat_inj', int.coe_nat_mod, int.coe_nat_mod,
 theorem modeq_of_dvd : (n:ℤ) ∣ b - a → a ≡ b [MOD n] := modeq_iff_dvd.2
 theorem dvd_of_modeq : a ≡ b [MOD n] → (n:ℤ) ∣ b - a := modeq_iff_dvd.1
 
+/-- A variant of `modeq_iff_dvd` with `nat` divisibility -/
+theorem modeq_iff_dvd' (h : a ≤ b) : a ≡ b [MOD n] ↔ n ∣ b - a :=
+by rw [modeq_iff_dvd, ←int.coe_nat_dvd, int.coe_nat_sub h]
+
 theorem mod_modeq (a n) : a % n ≡ a [MOD n] := nat.mod_mod _ _
 
 theorem modeq_of_dvd_of_modeq (d : m ∣ n) (h : a ≡ b [MOD n]) : a ≡ b [MOD m] :=
@@ -80,6 +96,7 @@ by rw [modeq_iff_dvd] at *; exact dvd.trans (dvd_mul_left (n : ℤ) (m : ℤ)) h
 theorem modeq_of_modeq_mul_right (m : ℕ) : a ≡ b [MOD n * m] → a ≡ b [MOD n] :=
 mul_comm m n ▸ modeq_of_modeq_mul_left _
 
+/-- The natural number less than `n*m` congruent to `a` mod `n` and `b` mod `m` -/
 def chinese_remainder (co : coprime n m) (a b : ℕ) : {k // k ≡ a [MOD n] ∧ k ≡ b [MOD m]} :=
 ⟨let (c, d) := xgcd n m in int.to_nat ((b * c * n + a * d * m) % (n * m)), begin
   rw xgcd_val, dsimp [chinese_remainder._match_1],