feat(data/int/order): delete int.order and prove all commented out le…

…mmas (#348)

algebra/archimedean.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro
 
 Archimedean groups and fields.
 -/
-import algebra.group_power data.rat data.int.order
+import algebra.group_power data.rat
 
 local infix ` • ` := add_monoid.smul
 
@@ -99,14 +99,14 @@ theorem ceil_lt_add_one (x : α) : (⌈x⌉ : α) < x + 1 :=
 by rw [← lt_ceil, ← int.cast_one, ceil_add_int]; apply lt_add_one
 
 lemma ceil_pos {a : α} : 0 < ⌈a⌉ ↔ 0 < a :=
-⟨ λ h, have ⌊-a⌋ < 0, from neg_of_neg_pos h, 
+⟨ λ h, have ⌊-a⌋ < 0, from neg_of_neg_pos h,
   pos_of_neg_neg $ lt_of_not_ge $ (not_iff_not_of_iff floor_nonneg).1 $ not_le_of_gt this,
  λ 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 :=
 if h : q > 0 then le_of_lt $ ceil_pos.2 h
-else 
+else
   have h' : q = 0, from le_antisymm (le_of_not_lt h) hq,
   by simp [h']
 

data/int/basic.lean

@@ -38,6 +38,8 @@ lemma coe_nat_ne_zero_iff_pos {n : ℕ} : (n : ℤ) ≠ 0 ↔ 0 < n :=
 ⟨λ h, nat.pos_of_ne_zero (coe_nat_ne_zero.1 h),
 λ h, (ne_of_lt (coe_nat_lt.2 h)).symm⟩
 
+lemma coe_nat_succ_pos (n : ℕ) : 0 < (n.succ : ℤ) := int.coe_nat_pos.2 (succ_pos n)
+
 /- succ and pred -/
 
 /-- Immediate successor of an integer: `succ n = n + 1` -/
@@ -718,6 +720,9 @@ units.ext_iff.1 $ nat.units_eq_one ⟨nat_abs u, nat_abs ↑u⁻¹,
 theorem units_eq_one_or (u : units ℤ) : u = 1 ∨ u = -1 :=
 by simpa [units.ext_iff, units_nat_abs] using nat_abs_eq u
 
+lemma units_inv_eq_self (u : units ℤ) : u⁻¹ = u :=
+(units_eq_one_or u).elim (λ h, h.symm ▸ rfl) (λ h, h.symm ▸ rfl)
+
 /- bitwise ops -/
 
 @[simp] lemma bodd_zero : bodd 0 = ff := rfl