feat(library/init/data/fin): add div

library/init/data/fin/ops.lean

@@ -43,6 +43,12 @@ end
 protected def mod : fin n → fin n → fin n
 | ⟨a, h₁⟩ ⟨b, h₂⟩ := ⟨a % b, modlt h₁ h₂⟩
 
+private lemma divlt {a b n : nat} (h : a < n) : a / b < n :=
+lt_of_le_of_lt (nat.div_le_self a b) h
+
+protected def div : fin n → fin n → fin n
+| ⟨a, h⟩ ⟨b, _⟩ := ⟨a / b, divlt h⟩
+
 protected def lt : fin n → fin n → Prop
 | ⟨a, _⟩ ⟨b, _⟩ := a < b
 
@@ -55,6 +61,7 @@ instance : has_add (fin n)         := ⟨fin.add⟩
 instance : has_sub (fin n)         := ⟨fin.sub⟩
 instance : has_mul (fin n)         := ⟨fin.mul⟩
 instance : has_mod (fin n)         := ⟨fin.mod⟩
+instance : has_div (fin n)         := ⟨fin.div⟩
 instance : has_lt (fin n)          := ⟨fin.lt⟩
 instance : has_le (fin n)          := ⟨fin.le⟩
 

library/init/data/nat/lemmas.lean

@@ -836,4 +836,21 @@ by simp [mod_one] at this; assumption
 protected lemma div_zero (n : ℕ) : n / 0 = 0 :=
 begin rw [div_def], simp [lt_irrefl] end
 
+protected lemma div_le_of_le_mul {m n : ℕ} : ∀ {k}, m ≤ k * n → m / k ≤ n
+| 0        h := by simp [nat.div_zero]; apply zero_le
+| (succ k) h :=
+  suffices succ k * (m / succ k) ≤ succ k * n, from le_of_mul_le_mul_left this (zero_lt_succ _),
+  calc
+    succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k) : le_add_left _ _
+                      ... = m                                  : by rw mod_add_div
+                      ... ≤ succ k * n                         : h
+
+protected lemma div_le_self : ∀ (m n : ℕ), m / n ≤ m
+| m 0        := by simp [nat.div_zero]; apply zero_le
+| m (succ n) :=
+  have m ≤ succ n * m, from calc
+    m  = 1 * m      : by simp
+   ... ≤ succ n * m : mul_le_mul_right _ (succ_le_succ (zero_le _)),
+  nat.div_le_of_le_mul this
+
 end nat

library/init/data/unsigned/ops.lean

@@ -14,6 +14,7 @@ instance : has_add unsigned  := ⟨fin.add⟩
 instance : has_sub unsigned  := ⟨fin.sub⟩
 instance : has_mul unsigned  := ⟨fin.mul⟩
 instance : has_mod unsigned  := ⟨fin.mod⟩
+instance : has_div unsigned  := ⟨fin.div⟩
 instance : has_lt unsigned   := ⟨fin.lt⟩
 instance : has_le unsigned   := ⟨fin.le⟩
 end unsigned