Hensel's lemma over the p-adic integers

algebra/archimedean.lean

@@ -104,7 +104,9 @@ lemma ceil_pos {a : α} : 0 < ⌈a⌉ ↔ 0 < a :=
  λ h, have -a < 0, from neg_neg_of_pos h,
   neg_pos_of_neg $ lt_of_not_ge $ (not_iff_not_of_iff floor_nonneg).2 $ not_le_of_gt this ⟩
 
-lemma ceil_nonneg {q : ℚ} (hq : q ≥ 0) : ⌈q⌉ ≥ 0 :=
+@[simp] theorem ceil_zero : ⌈(0 : α)⌉ = 0 := by simp [ceil]
+
+lemma ceil_nonneg [decidable_rel ((<) : α → α → Prop)] {q : α} (hq : q ≥ 0) : ⌈q⌉ ≥ 0 :=
 if h : q > 0 then le_of_lt $ ceil_pos.2 h
 else
   have h' : q = 0, from le_antisymm (le_of_not_lt h) hq,
@@ -233,6 +235,18 @@ begin
        ← div_lt_iff' (sub_pos.2 h), one_div_eq_inv]
 end
 
+theorem exists_nat_one_div_lt {ε : α} (hε : ε > 0) : ∃ n : ℕ, 1 / (n + 1: α) < ε :=
+begin
+  cases archimedean_iff_nat_lt.1 (by apply_instance) (1/ε) with n hn,
+  existsi n,
+  apply div_lt_of_mul_lt_of_pos,
+  { simp, apply add_pos_of_pos_of_nonneg zero_lt_one, apply nat.cast_nonneg },
+  { apply (div_lt_iff' hε).1,
+    transitivity,
+    { exact hn },
+    { simp [zero_lt_one] }}
+end
+
 include α
 @[simp] theorem rat.cast_floor (x : ℚ) :
   by haveI := archimedean.floor_ring α; exact ⌊(x:α)⌋ = ⌊x⌋ :=

algebra/field_power.lean

@@ -37,7 +37,6 @@ lemma fpow_ne_zero_of_ne_zero {a : α} (ha : a ≠ 0) : ∀ (z : ℤ), fpow a z
 | (of_nat n) := pow_ne_zero _ ha
 | -[1+n] := one_div_ne_zero $ pow_ne_zero _ ha
 
-
 @[simp] lemma fpow_zero {a : α} : fpow a 0 = 1 :=
 pow_zero _
 
@@ -58,6 +57,14 @@ lemma zero_fpow : ∀ z : ℤ, z ≠ 0 → fpow (0 : α) z = 0
   have h1 : (0 : α) ^ (n+1) = 0, from zero_mul _,
   by simp [fpow, h1]
 
+lemma fpow_neg (a : α) : ∀ n, fpow a (-n) = 1 / fpow a n
+| (of_nat 0) := by simp [of_nat_zero]
+| (of_nat (n+1)) := rfl
+| -[1+n] := show fpow a (n+1) = 1 / (1 / fpow a (n+1)), by rw one_div_one_div
+
+lemma fpow_sub {a : α} (ha : a ≠ 0) (z1 z2 : ℤ) : fpow a (z1 - z2) = fpow a z1 / fpow a z2 :=
+by rw [sub_eq_add_neg, fpow_add ha, fpow_neg, ←div_eq_mul_one_div]
+
 end discrete_field_power
 
 section ordered_field_power
@@ -69,6 +76,9 @@ lemma fpow_nonneg_of_nonneg {a : α} (ha : a ≥ 0) : ∀ (z : ℤ), fpow a z 
 | (of_nat n) := pow_nonneg ha _
 | -[1+n] := div_nonneg' zero_le_one $ pow_nonneg ha _
 
+lemma fpow_pos_of_pos {a : α} (ha : a > 0) : ∀ (z : ℤ), fpow a z > 0
+| (of_nat n) := pow_pos ha _
+| -[1+n] := div_pos zero_lt_one $ pow_pos ha _
 
 lemma fpow_le_of_le {x : α} (hx : 1 ≤ x) {a b : ℤ} (h : a ≤ b) : fpow x a ≤ fpow x b :=
 begin
@@ -102,4 +112,28 @@ begin
   simpa [hfle] using this
 end
 
+lemma fpow_le_one_of_nonpos {p : α} (hp : p ≥ 1) {z : ℤ} (hz : z ≤ 0) : fpow p z ≤ 1 :=
+calc fpow p z ≤ fpow p 0 : fpow_le_of_le hp hz
+          ... = 1        : by simp
+
+lemma fpow_ge_one_of_nonneg {p : α} (hp : p ≥ 1) {z : ℤ} (hz : z ≥ 0) : fpow p z ≥ 1 :=
+calc fpow p z ≥ fpow p 0 : fpow_le_of_le hp hz
+          ... = 1        : by simp
+
 end ordered_field_power
+
+lemma one_lt_pow {α} [linear_ordered_semiring α] {p : α} (hp : p > 1) : ∀ {n : ℕ}, 1 ≤ n → 1 < p ^ n
+| 1 h := by simp; assumption
+| (k+2) h :=
+  begin
+    rw ←one_mul (1 : α),
+    apply mul_lt_mul,
+    { assumption },
+    { apply le_of_lt, simpa using one_lt_pow (nat.le_add_left 1 k)},
+    { apply zero_lt_one },
+    { apply le_of_lt (lt_trans zero_lt_one hp) }
+  end
+
+lemma one_lt_fpow {α}  [discrete_linear_ordered_field α] {p : α} (hp : p > 1) :
+  ∀ z : ℤ, z > 0 → 1 < fpow p z
+| (int.of_nat n) h := one_lt_pow hp (nat.succ_le_of_lt (int.lt_of_coe_nat_lt_coe_nat h))

algebra/group_power.lean

@@ -440,6 +440,38 @@ calc a ^ n = a ^ n * 1 : by simp
     (pow_nonneg (le_trans zero_le_one ha) _)
   ... = a ^ m : by rw [←hk, pow_add]
 
+lemma pow_le_pow_of_le_left  {a b : α} (ha : 0 ≤ a) (hab : a ≤ b) : ∀ i : ℕ, a^i ≤ b^i
+| 0 := by simp
+| (k+1) := mul_le_mul hab (pow_le_pow_of_le_left _) (pow_nonneg ha _) (le_trans ha hab)
+
+private lemma pow_lt_pow_of_lt_one_aux {a : α} (h : 0 < a) (ha : a < 1) (i : ℕ) :
+  ∀ k : ℕ, a ^ (i + k + 1) < a ^ i
+| 0 := begin simp, rw ←one_mul (a^i), exact mul_lt_mul ha (le_refl _) (pow_pos h _) zero_le_one end
+| (k+1) :=
+  begin
+    rw ←one_mul (a^i),
+    apply mul_lt_mul ha _ _ zero_le_one,
+    { apply le_of_lt, apply pow_lt_pow_of_lt_one_aux },
+    { show 0 < a ^ (i + (k + 1) + 0), apply pow_pos h }
+  end
+
+private lemma pow_le_pow_of_le_one_aux {a : α}  (h : 0 ≤ a) (ha : a ≤ 1) (i : ℕ) :
+  ∀ k : ℕ, a ^ (i + k) ≤ a ^ i
+| 0 := by simp
+| (k+1) := by rw [←add_assoc, ←one_mul (a^i)];
+              exact mul_le_mul ha (pow_le_pow_of_le_one_aux _) (pow_nonneg h _) zero_le_one
+
+lemma pow_lt_pow_of_lt_one  {a : α} (h : 0 < a) (ha : a < 1)
+  {i j : ℕ} (hij : i < j) : a ^ j < a ^ i :=
+let ⟨k, hk⟩ := nat.exists_eq_add_of_lt hij in
+by rw hk; exact pow_lt_pow_of_lt_one_aux h ha _ _
+
+lemma pow_le_pow_of_le_one  {a : α} (h : 0 ≤ a) (ha : a ≤ 1)
+  {i j : ℕ} (hij : i ≤ j) : a ^ j ≤ a ^ i :=
+let ⟨k, hk⟩ := nat.exists_eq_add_of_le hij in
+by rw hk; exact pow_le_pow_of_le_one_aux h ha _ _
+
+
 end linear_ordered_semiring
 
 theorem pow_two_nonneg [linear_ordered_ring α] (a : α) : 0 ≤ a ^ 2 :=
@@ -458,3 +490,9 @@ lemma units_pow_eq_pow_mod_two (u : units ℤ) (n : ℕ) : u ^ n = u ^ (n % 2) :
 by conv {to_lhs, rw ← nat.mod_add_div n 2}; simp [pow_add, pow_mul, units_pow_two]
 
 end int
+
+@[simp] lemma neg_square {α} [ring α] (z : α) : (-z)^2 = z^2 :=
+by simp [pow, monoid.pow]
+
+lemma div_sq_cancel {α} [field α] {a : α} (ha : a ≠ 0) (b : α) : a^2 * b / a = a * b :=
+by rw [pow_two, mul_assoc, mul_div_cancel_left _ ha]

algebra/ordered_ring.lean

@@ -81,6 +81,22 @@ lemma one_lt_mul {a b : α} (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b :=
 lemma mul_le_one {a b : α} (ha : a ≤ 1) (hb' : 0 ≤ b) (hb : b ≤ 1) : a * b ≤ 1 :=
 begin rw ← one_mul (1 : α), apply mul_le_mul; {assumption <|> apply zero_le_one} end
 
+lemma mul_le_iff_le_one_left {a b : α} (hb : b > 0) : a * b ≤ b ↔ a ≤ 1 :=
+⟨ λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_left hb).2 (not_lt_of_ge h)),
+  λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_left hb).1 (not_lt_of_ge h)) ⟩
+
+lemma mul_lt_iff_lt_one_left {a b : α} (hb : b > 0) : a * b < b ↔ a < 1 :=
+⟨ λ h, lt_of_not_ge (mt (le_mul_iff_one_le_left hb).2 (not_le_of_gt h)),
+  λ h, lt_of_not_ge (mt (le_mul_iff_one_le_left hb).1 (not_le_of_gt h)) ⟩
+
+lemma mul_le_iff_le_one_right {a b : α} (hb : b > 0) : b * a ≤ b ↔ a ≤ 1 :=
+⟨ λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_right hb).2 (not_lt_of_ge h)),
+  λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_right hb).1 (not_lt_of_ge h)) ⟩
+
+lemma mul_lt_iff_lt_one_right {a b : α} (hb : b > 0) : b * a < b ↔ a < 1 :=
+⟨ λ h, lt_of_not_ge (mt (le_mul_iff_one_le_right hb).2 (not_le_of_gt h)),
+  λ h, lt_of_not_ge (mt (le_mul_iff_one_le_right hb).1 (not_le_of_gt h)) ⟩
+
 end linear_ordered_semiring
 
 instance linear_ordered_semiring.to_no_top_order {α : Type*} [linear_ordered_semiring α] :

analysis/limits.lean

@@ -134,6 +134,22 @@ by_cases
         tendsto_inverse_at_top_nhds_0,
     tendsto_cong this $ univ_mem_sets' $ by simp *)
 
+lemma tendsto_coe_iff {f : ℕ → ℕ} : tendsto (λ n, (f n : ℝ)) at_top at_top ↔ tendsto f at_top at_top :=
+⟨ λ h, tendsto_infi.2 $ λ i, tendsto_principal.2
+    (have _, from tendsto_infi.1 h i, by simpa using tendsto_principal.1 this),
+  λ h, tendsto.comp h tendsto_of_nat_at_top_at_top ⟩
+
+lemma tendsto_pow_at_top_at_top_of_gt_1_nat {k : ℕ} (h : k > 1) : tendsto (λn:ℕ, k ^ n) at_top at_top :=
+tendsto_coe_iff.1 $
+  have hr : (k : ℝ) > 1, from show (k : ℝ) > (1 : ℕ), from nat.cast_lt.2 h,
+  by simpa using tendsto_pow_at_top_at_top_of_gt_1 hr
+
+lemma tendsto_inverse_at_top_nhds_0_nat : tendsto (λ n : ℕ, (n : ℝ)⁻¹) at_top (nhds 0) :=
+tendsto.comp (tendsto_coe_iff.2 tendsto_id) tendsto_inverse_at_top_nhds_0
+
+lemma tendsto_one_div_at_top_nhds_0_nat : tendsto (λ n : ℕ, 1/(n : ℝ)) at_top (nhds 0) :=
+by simpa only [inv_eq_one_div] using tendsto_inverse_at_top_nhds_0_nat
+
 lemma sum_geometric' {r : ℝ} (h : r ≠ 0) :
   ∀{n}, (finset.range n).sum (λi, (r + 1) ^ i) = ((r + 1) ^ n - 1) / r
 | 0     := by simp [zero_div]

analysis/normed_space.lean

@@ -84,6 +84,9 @@ abs_le.2 $ and.intro
 lemma dist_norm_norm_le (g h : α) : dist ∥g∥ ∥h∥ ≤ ∥g - h∥ :=
 abs_norm_sub_norm_le g h
 
+lemma norm_sub_rev (g h : α) : ∥g - h∥ = ∥h - g∥ :=
+by rw ←norm_neg; simp
+
 section nnnorm
 
 def nnnorm (a : α) : nnreal := ⟨norm a, norm_nonneg a⟩
@@ -179,6 +182,13 @@ instance normed_ring.to_normed_group [β : normed_ring α] : normed_group α :=
 lemma norm_mul {α : Type*} [normed_ring α] (a b : α) : (∥a*b∥) ≤ (∥a∥) * (∥b∥) :=
 normed_ring.norm_mul _ _
 
+lemma norm_pow {α : Type*} [normed_ring α] (a : α) : ∀ {n : ℕ}, n > 0 → ∥a^n∥ ≤ ∥a∥^n
+| 1 h := by simp
+| (n+2) h :=
+  le_trans (norm_mul a (a^(n+1)))
+           (mul_le_mul (le_refl _)
+                       (norm_pow (nat.succ_pos _)) (norm_nonneg _) (norm_nonneg _))
+
 instance prod.normed_ring [normed_ring α] [normed_ring β] : normed_ring (α × β) :=
 { norm_mul := assume x y,
   calc
@@ -192,6 +202,43 @@ instance prod.normed_ring [normed_ring α] [normed_ring β] : normed_ring (α ×
   ..prod.normed_group }
 end normed_ring
 
+instance normed_ring_top_monoid [normed_ring α] : topological_monoid α :=
+⟨ continuous_iff_tendsto.2 $ λ x, tendsto_iff_norm_tendsto_zero.2 $
+    have ∀ e : α × α, e.fst * e.snd - x.fst * x.snd =
+      e.fst * e.snd - e.fst * x.snd + (e.fst * x.snd - x.fst * x.snd), by intro; rw sub_add_sub_cancel,
+    begin
+      apply squeeze_zero,
+      { intro, apply norm_nonneg },
+      { simp only [this], intro, apply norm_triangle },
+      { rw ←zero_add (0 : ℝ), apply tendsto_add,
+        { apply squeeze_zero,
+          { intro, apply norm_nonneg },
+          { intro t, show ∥t.fst * t.snd - t.fst * x.snd∥ ≤ ∥t.fst∥ * ∥t.snd - x.snd∥,
+            rw ←mul_sub, apply norm_mul },
+          { rw ←mul_zero (∥x.fst∥), apply tendsto_mul,
+            { apply continuous_iff_tendsto.1,
+              apply continuous.comp,
+              { apply continuous_fst },
+              { apply continuous_norm }},
+            { apply tendsto_iff_norm_tendsto_zero.1,
+              apply continuous_iff_tendsto.1,
+              apply continuous_snd }}},
+        { apply squeeze_zero,
+          { intro, apply norm_nonneg },
+          { intro t, show ∥t.fst * x.snd - x.fst * x.snd∥ ≤ ∥t.fst - x.fst∥ * ∥x.snd∥,
+            rw ←sub_mul, apply norm_mul },
+          { rw ←zero_mul (∥x.snd∥), apply tendsto_mul,
+            { apply tendsto_iff_norm_tendsto_zero.1,
+              apply continuous_iff_tendsto.1,
+              apply continuous_fst },
+            { apply tendsto_const_nhds }}}}
+    end ⟩
+
+instance normed_top_ring [normed_ring α] : topological_ring α :=
+⟨ continuous_iff_tendsto.2 $ λ x, tendsto_iff_norm_tendsto_zero.2 $
+    have ∀ e : α, -e - -x = -(e - x), by intro; simp,
+    by simp only [this, norm_neg]; apply lim_norm ⟩
+
 section normed_field
 
 class normed_field (α : Type*) extends has_norm α, discrete_field α, metric_space α :=
@@ -201,6 +248,31 @@ class normed_field (α : Type*) extends has_norm α, discrete_field α, metric_s
 instance normed_field.to_normed_ring [i : normed_field α] : normed_ring α :=
 { norm_mul := by finish [i.norm_mul], ..i }
 
+@[simp] lemma norm_one {α : Type*} [normed_field α] : ∥(1 : α)∥ = 1 :=
+have  ∥(1 : α)∥ * ∥(1 : α)∥ = ∥(1 : α)∥ * 1, by calc
+ ∥(1 : α)∥ * ∥(1 : α)∥ = ∥(1 : α) * (1 : α)∥ : by rw normed_field.norm_mul
+                  ... = ∥(1 : α)∥ * 1 : by simp,
+eq_of_mul_eq_mul_left (ne_of_gt ((norm_pos_iff _).2 (by simp))) this
+
+@[simp] lemma norm_div {α : Type*} [normed_field α] (a b : α) : ∥a/b∥ = ∥a∥/∥b∥ :=
+if hb : b = 0 then by simp [hb] else
+begin
+  apply eq_div_of_mul_eq,
+  { apply ne_of_gt, apply (norm_pos_iff _).mpr hb },
+  { rw [←normed_field.norm_mul, div_mul_cancel _ hb] }
+end
+
+@[simp] lemma norm_inv {α : Type*} [normed_field α] (a : α) : ∥a⁻¹∥ = ∥a∥⁻¹ :=
+by simp only [inv_eq_one_div, norm_div, norm_one]
+
+@[simp] lemma normed_field.norm_pow {α : Type*} [normed_field α] (a : α) :
+  ∀ n : ℕ, ∥a^n∥ = ∥a∥^n
+| 0 := by simp
+| (k+1) := calc
+  ∥a ^ (k + 1)∥ = ∥a*(a^k)∥ : rfl
+           ... = ∥a∥*∥a^k∥ : by rw normed_field.norm_mul
+           ... = ∥a∥ ^ (k + 1) : by rw normed_field.norm_pow; simp [pow, monoid.pow]
+
 instance : normed_field ℝ :=
 { norm := λ x, abs x,
   dist_eq := assume x y, rfl,

analysis/polynomial.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Robert Y. Lewis
+
+Analytic facts about polynomials.
+-/
+
+import analysis.topology.topological_structures data.polynomial
+
+lemma polynomial.continuous_eval {α} [comm_semiring α] [decidable_eq α] [topological_space α]
+  [topological_semiring α] (p : polynomial α) : continuous (λ x, p.eval x) :=
+begin
+  apply p.induction,
+  { convert continuous_const,
+    ext, show polynomial.eval x 0 = 0, from rfl },
+  { intros a b f haf hb hcts,
+    simp only [polynomial.eval_add],
+    refine continuous_add _ hcts,
+    have : ∀ x, finsupp.sum (finsupp.single a b) (λ (e : ℕ) (a : α), a * x ^ e) = b * x ^a,
+      from λ x, finsupp.sum_single_index (by simp),
+    convert continuous_mul _ _,
+    { ext, apply this },
+    { apply_instance },
+    { apply continuous_const },
+    { apply continuous_pow }}
+end

analysis/topology/topological_structures.lean

@@ -42,6 +42,10 @@ lemma continuous_mul [topological_space β] {f : β → α} {g : β → α}
   continuous (λx, f x * g x) :=
 (hf.prod_mk hg).comp continuous_mul'
 
+lemma continuous_pow : ∀ n : ℕ, continuous (λ a : α, a ^ n)
+| 0 := by simpa using continuous_const
+| (k+1) := show continuous (λ (a : α), a * a ^ k), from continuous_mul continuous_id (continuous_pow _)
+
 lemma tendsto_mul' {a b : α} : tendsto (λp:α×α, p.fst * p.snd) (nhds (a, b)) (nhds (a * b)) :=
 continuous_iff_tendsto.mp (topological_monoid.continuous_mul α) (a, b)
 

data/finsupp.lean

@@ -391,6 +391,11 @@ finset.sum_add_distrib
   {h : α → β → γ} : f.sum (λa b, - h a b) = - f.sum h :=
 finset.sum_hom (@has_neg.neg γ _) neg_zero (assume a b, neg_add _ _)
 
+@[simp] lemma sum_sub [add_comm_monoid β] [add_comm_group γ] {f : α →₀ β}
+  {h₁ h₂ : α → β → γ} :
+  f.sum (λa b, h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂ :=
+by rw [sub_eq_add_neg, ←sum_neg, ←sum_add]; refl
+
 @[simp] lemma sum_single [add_comm_monoid β] {f : α →₀ β} :
   f.sum single = f :=
 have ∀a:α, f.sum (λa' b, ite (a' = a) b 0) =

data/int/basic.lean

@@ -582,22 +582,25 @@ lemma dvd_nat_abs_of_of_nat_dvd {a : ℕ} : ∀ {z : ℤ} (haz : ↑a ∣ z), a
   have haz' : (↑a:ℤ) ∣ (↑(k+1):ℤ), from dvd_of_dvd_neg haz,
   int.coe_nat_dvd.1 haz'
 
-lemma pow_div_of_le_of_pow_div_int {p m n : ℕ} {k : ℤ} (hmn : m ≤ n) (hdiv : ↑(p ^ n) ∣ k) :
+lemma pow_dvd_of_le_of_pow_dvd {p m n : ℕ} {k : ℤ} (hmn : m ≤ n) (hdiv : ↑(p ^ n) ∣ k) :
       ↑(p ^ m) ∣ k :=
 begin
   induction k,
     { apply int.coe_nat_dvd.2,
-      apply pow_div_of_le_of_pow_div hmn,
+      apply pow_dvd_of_le_of_pow_dvd hmn,
       apply int.coe_nat_dvd.1 hdiv },
     { change -[1+k] with -(↑(k+1) : ℤ),
       apply dvd_neg_of_dvd,
       apply int.coe_nat_dvd.2,
-      apply pow_div_of_le_of_pow_div hmn,
+      apply pow_dvd_of_le_of_pow_dvd hmn,
       apply int.coe_nat_dvd.1,
       apply dvd_of_dvd_neg,
       exact hdiv }
 end
 
+lemma dvd_of_pow_dvd {p k : ℕ} {m : ℤ} (hk : 1 ≤ k) (hpk : ↑(p^k) ∣ m) : ↑p ∣ m := 
+by rw ←nat.pow_one p; exact pow_dvd_of_le_of_pow_dvd hk hpk
+
 /- / and ordering -/
 
 protected theorem div_mul_le (a : ℤ) {b : ℤ} (H : b ≠ 0) : a / b * b ≤ a :=

data/int/modeq.lean

@@ -77,6 +77,29 @@ by rw [mul_comm a, mul_comm b]; exact modeq_mul_left c h
 theorem modeq_mul (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a * c ≡ b * d [ZMOD n] :=
 (modeq_mul_left _ h₂).trans (modeq_mul_right _ h₁)
 
+theorem modeq_add_fac {a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) : a + n*c ≡ b [ZMOD n] :=
+calc a + n*c ≡ b + n*c [ZMOD n] : int.modeq.modeq_add ha (int.modeq.refl _) 
+         ... ≡ b + 0 [ZMOD n] : int.modeq.modeq_add (int.modeq.refl _) (int.modeq.modeq_zero_iff.2 (dvd_mul_right _ _))
+         ... ≡ b [ZMOD n] : by simp
+
+open nat 
+lemma mod_coprime {a b : ℕ} (hab : coprime a b) : ∃ y : ℤ, a * y ≡ 1 [ZMOD b] :=
+⟨ gcd_a a b, 
+  have hgcd : nat.gcd a b = 1, from coprime.gcd_eq_one hab,
+  calc
+   ↑a * gcd_a a b ≡ ↑a*gcd_a a b + ↑b*gcd_b a b [ZMOD ↑b] : int.modeq.symm $ modeq_add_fac _ $ int.modeq.refl _
+              ... ≡ 1 [ZMOD ↑b] : by rw [←gcd_eq_gcd_ab, hgcd]; reflexivity ⟩
+
+lemma exists_unique_equiv (a : ℤ) {b : ℤ} (hb : b > 0) : ∃ z : ℤ, 0 ≤ z ∧ z < b ∧ z ≡ a [ZMOD b] :=
+⟨ a % b, int.mod_nonneg _ (ne_of_gt hb), 
+  have a % b < abs b, from int.mod_lt _ (ne_of_gt hb),
+  by rwa abs_of_pos hb at this, 
+  by simp [int.modeq] ⟩
+
+lemma exists_unique_equiv_nat (a : ℤ) {b : ℤ} (hb : b > 0) : ∃ z : ℕ, ↑z < b ∧ ↑z ≡ a [ZMOD b] :=
+let ⟨z, hz1, hz2, hz3⟩ := exists_unique_equiv a hb in 
+⟨z.nat_abs, by split; rw [←int.of_nat_eq_coe, int.of_nat_nat_abs_eq_of_nonneg hz1]; assumption⟩
+
 theorem modeq_of_modeq_mul_left (m : ℤ) (h : a ≡ b [ZMOD m * n]) : a ≡ b [ZMOD n] :=
 by rw [modeq_iff_dvd] at *; exact dvd.trans (dvd_mul_left n m) h