order.lean

import .power

section order

definition minimal_lt (P : ℕ → Prop) [decidable_pred P]
  : ℕ → option (Σ' k : ℕ, P k)
| 0 := none
| (n+1) := minimal_lt n
        <|> (if h' : P n then some ⟨n, h'⟩ else none)

lemma option.alt_eq_none {α} : ∀ o o' : option α,
  (o <|> o') = none ↔ o = none ∧ o' = none :=
by intros; cases o; cases o'; simp [(<|>), option.orelse]

lemma option.alt_eq_some {α} : ∀ (o o' : option α) (a : α),
  (o <|> o') = some a
  ↔ o = some a ∨ (o = none ∧ o' = some a) :=
by intros; cases o; cases o'; simp [(<|>), option.orelse]

lemma option.none_alt_eq_some {α} : ∀ (o : option α) (a : α),
  (none <|> o) = some a ↔ o = some a := by intros; rw option.alt_eq_some; simp

lemma minimal_lt_spec1 {P : ℕ → Prop} [decidable_pred P]
  : ∀ n, minimal_lt P n = none ↔ (∀ k < n, ¬ P k) :=
begin
  intro, induction n with n ih; simp [minimal_lt],
  case nat.zero { intros k hk, cases hk },
  case nat.succ {
    rw option.alt_eq_none,
    by_cases P n,
    { rw dif_pos h, rw ih, simp, intro hneg, 
      specialize hneg n _ h, assumption, apply nat.lt_succ_self, },
    { rw dif_neg h, rw ih, simp, constructor; intro h',
      { intro k, by_cases k < n, intro _, apply h', assumption,
        intro h'', cases eq_or_lt_of_not_lt h, rw h_1, assumption,
        exfalso, cases h'', apply nat.lt_irrefl _ h_1,
        apply h, assumption },
      { intros, apply h', transitivity, assumption, apply nat.lt_succ_self } } }
end

lemma minimal_lt_spec2 {P : ℕ → Prop} [decidable_pred P]
  : ∀ n k h, minimal_lt P n = some ⟨k, h⟩
           ↔ (k < n ∧ (∀ j, j < k → ¬ P j)) :=
begin
  intros n, induction n with n ih; intros k h; simp [minimal_lt],
  { intro h, cases h, apply nat.not_lt_zero, assumption },
  { destruct minimal_lt P n,
    { intro H, rw H,
      rw minimal_lt_spec1 at H,
      rw option.none_alt_eq_some,
      by_cases P n,
      { rw dif_pos h, transitivity n = k,
        { constructor; intro h, cases h, refl, congr, assumption },
        { constructor; intro h, 
          constructor, rw h, apply nat.lt_succ_self,
          intros j hj, rw ← h at hj, apply H, assumption,
          cases h, cases h_left, refl,
          exfalso, apply H k; assumption } },
      { rw dif_neg h, simp, intro h',
        cases h', cases h'_left, contradiction,
        apply H, assumption, assumption } },
    { intros val hval, cases val with j hj,
      rw hval, rw ih at hval, simp [(<|>), option.orelse],
      transitivity j = k,
      { constructor; intro h; cases h, assumption, constructor; refl },
      constructor; intro h, 
      { subst h, constructor,
        { transitivity n, exact hval.left, apply nat.lt_succ_self },
        exact hval.right },
      { cases nat.lt_trichotomy j k,
        { exfalso, apply h.right; assumption },
        cases h_1, assumption,
        { exfalso, apply hval.right; assumption } } } }
end


def dec_order {G} [group G] [decidable_eq G] (g : G) (bound : ℕ) (hgt : bound > 0) (h : g^bound = 1) : ℕ :=
option.get_or_else (option.map psigma.fst (minimal_lt (λ k, k > 0 ∧ g^k = 1) (bound + 1))) bound

lemma dec_order_spec {G} [group G] [decidable_eq G] (g : G) (bound : ℕ) (hgt : bound > 0) (h : g^bound = 1)
  : dec_order g bound hgt h ≤ bound
  ∧ 0 < dec_order g bound hgt h
  ∧ (g^(dec_order g bound hgt h) = 1)
  ∧ (∀ j, j < dec_order g bound hgt h → g^j = 1 → j = 0) :=
begin
  destruct minimal_lt (λ (k : ℕ), k > 0 ∧ g ^ k = 1) (bound + 1),
  { simp [dec_order],
    intro h', rw h', rw minimal_lt_spec1 at h',
    exfalso, apply h', apply nat.lt_succ_self, constructor; assumption },
  { intros val hval, cases val with n hn, cases hn with hngt hn, 
    have : dec_order g bound hgt h = n,
    { simp [dec_order],  rw hval, simp [option.map, option.bind, option.get_or_else] },
    rw this, rw minimal_lt_spec2 at hval, constructor,
    { apply nat.le_of_lt_succ, exact hval.left },
    { constructor, assumption, constructor, assumption, intros j hjlt hj, 
      suffices : ¬ j > 0,
      { cases nat.zero_le j, refl, exfalso, apply this, apply nat.zero_lt_succ },
      suffices : ¬(j > 0 ∧ g ^ j = 1),
      { rw decidable.not_and_iff_or_not at this, cases this, assumption, contradiction },
      apply hval.right, assumption } }
end

section classical

inductive order {G} [group G] (g : G)
| infinite : (∀ n : ℕ, g^n = 1 → n = 0) → order
| finite : ∀ n : ℕ, 0 < n → g^n = 1 → (∀ k : ℕ, k < n → g^k = 1 → k = 0) → order

local attribute [instance] classical.prop_decidable

def power_zero_of_no_finite_order {G} [group G] (g : G)
  (h : ¬∃ (n : ℕ), n > 0 ∧ g ^ n = 1) (n : ℕ) (h' : g ^ n = 1) : n = 0 :=
begin
  by_contra, apply h, existsi n,
  constructor, apply nat.lt_of_le_and_ne,
  apply nat.zero_le, apply ne.symm, assumption, assumption
end

def no_infinite_order_of_finite_order {G} [group G] (g : G)
  (h : ∃ (n : ℕ), n > 0 ∧ g ^ n = 1) : ¬ ∀ (n : ℕ) (h' : g ^ n = 1), n = 0 :=
begin
  intro h', cases h with n hn, cases hn with hgt hn,
  rw h' n hn at hgt, apply nat.lt_irrefl _ hgt
end

noncomputable def classical.order {G} [group G] (g : G) : order g := 
if h : ∃ n, n > 0 ∧ g^n = 1
then order.finite (dec_order g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right)
                  (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.left
                  (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.right.left
                  (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.right.right
else order.infinite $ power_zero_of_no_finite_order g h

noncomputable def classical.order' {G} [group G] (g : G) : ℕ := 
match classical.order g with
| order.infinite _ := 0
| order.finite n _ _ _ := n
end

lemma classical.order'_spec1 {G} [group G] (g : G)
  : classical.order' g = 0 ↔ ∀ n, g^n = 1 → n = 0 :=
begin
  dsimp [classical.order', classical.order],
  by_cases h : ∃ n, n > 0 ∧ g^n = 1,
  { rw dif_pos h, simp [classical.order'._match_1],
    transitivity false,
    { rw iff_false, rw (_ : ∀ n, ¬ (n = 0) ↔ 0 < n), 
      apply and.left (and.right (dec_order_spec g _ _ _)),
      intro n; cases n, simp *, apply nat.lt_irrefl,
      transitivity true, rw iff_true, apply nat.succ_ne_zero,
      rw true_iff, apply nat.zero_lt_succ },
    { rw false_iff, apply no_infinite_order_of_finite_order g h, } },
  { rw dif_neg h, simp [classical.order'._match_1],
    apply power_zero_of_no_finite_order g h }
end

lemma classical.order'_spec2 {G} [group G] (g : G)
  : ∀ n, 0 < n → (classical.order' g = n
                 ↔ g^n = 1 ∧ (∀ k : ℕ, k < n → g^k = 1 → k = 0)) :=
begin
  intros n hn,
  dsimp [classical.order', classical.order],
  by_cases h : ∃ n, n > 0 ∧ g^n = 1,
  { rw dif_pos h, simp [classical.order'._match_1],
     constructor, { intro h, subst h, apply (dec_order_spec g _ _ _).right.right },
     intro h', cases nat.lt_trichotomy _ n,
     tactic.swap, cases h_1, exact h_1,
     { suffices : n = 0, { exfalso, rw this at hn, apply nat.lt_irrefl _ hn },
       apply (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.right.right,
       assumption, exact h'.left },
     { suffices : dec_order g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right = 0,
       have this' := (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.left, 
       rw this at this', exfalso, apply nat.lt_irrefl _ this',
       apply h'.right, assumption, apply (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.right.left } },
  { rw dif_neg h, simp [classical.order'._match_1], transitivity false,
    { rw iff_false, intro h, rw h at hn, apply nat.lt_irrefl _ hn },
    { rw false_iff, intro h', apply h,
      existsi n, constructor, assumption, exact h'.left } }
end

end classical

def cyclic_subgroup {G} [group G] (g : G) : set G :=
  { h : G | ∃ n : ℤ, h = g^^n }

end order

pigeonhole.lean

lemma option.eq_some_of_get {α}
  : ∀ {o : option α} (h : option.is_some o), o = some (option.get h) :=
by { intros, cases o, cases h, simp [option.get] }

lemma option.eq_none_of_not_is_some {α}
  : ∀ {o : option α} (h : ¬ option.is_some o), o = none :=
by { intros, cases o, refl, simp [option.is_some] at h, contradiction }

def fin.up {n} (x : fin n) : fin (n+1) := fin.mk x.val $
  nat.lt_trans x.is_lt (nat.lt_succ_self _)

lemma fin.up_val {n} (x : fin n) : x.up.val = x.val := rfl

lemma fin.succ_val {n} (x : fin n)
  : x.succ.val = x.val + 1 := by cases x; simp [fin.succ]

def fin.down {n} (x : fin (n+1)) (hx : x.val ≠ n) : fin n := fin.mk x.val $
  nat.lt_of_le_and_ne (nat.le_of_lt_succ x.is_lt) hx

lemma fin.down_val {n} (x : fin (n+1)) (hx : x.val ≠ n) : (fin.down x hx).val = x.val := rfl

lemma fin.down_inj {n} (x y : fin (n+1)) (hx : x.val ≠ n) (hy : y.val ≠ n)
  : fin.down x hx = fin.down y hy → x = y :=
begin
  intro h, apply fin.eq_of_veq,
  rw [← fin.down_val, ← fin.down_val, h]
end

lemma lt_one_iff_eq_zero : ∀ n : ℕ, n < 1 ↔ n = 0 :=
begin
  intro n, cases n, { simp, apply nat.lt_succ_self },
  { transitivity false; rw iff_false <|> rw false_iff;
    intro h, cases nat.lt_of_succ_lt_succ h, cases h }
end

instance : subsingleton (fin 1) := subsingleton.intro $ by {
  intros, cases a with a, cases b with b,
  apply fin.eq_of_veq, simp,
  rw lt_one_iff_eq_zero at *, transitivity 0,
  assumption, symmetry, assumption
}

def get_maximal_sat' {α} {n : ℕ} (P : α → Prop) [decidable_pred P] (f : fin n → α)
  : ∀ (k : ℕ), k ≤ n → option (fin n)
| 0 := λ _, none
| (k+1) := λ h, if P (f ⟨k, h⟩)
                then some ⟨k, h⟩
                else get_maximal_sat' k (nat.le_trans (nat.le_of_lt $ nat.lt_succ_self k) h)

lemma get_maximal_sat'_spec_none {α} {n : ℕ} (P : α → Prop) [decidable_pred P] (f : fin n → α)
  : ∀ (k : ℕ) (hk : k ≤ n), (get_maximal_sat' P f k hk = none)
                          ↔ (∀ j (hj : j < k), ¬ (P (f ⟨j, nat.lt_of_lt_of_le hj hk⟩))) :=
begin
  intros k hk, induction k with k ih; simp [get_maximal_sat'],
  { intros, cases hj },
  { by_cases P (f ⟨k, hk⟩),
    { rw if_pos h, simp, intros h', apply h' k,
      assumption, apply nat.lt_succ_self },
    { rw if_neg h, specialize ih (nat.le_of_succ_le hk),
      rw ih, constructor; intros h' j hjk hjP; apply h' j,
      assumption,
      { apply nat.lt_of_le_and_ne, apply nat.le_of_lt_succ hjk,
        intro h', apply h, subst h', assumption },
      assumption, apply nat.lt_succ_of_lt, assumption } }
end

lemma get_maximal_sat'_spec_some1 {α} {n : ℕ} (P : α → Prop) [decidable_pred P] (f : fin n → α)
  : ∀ (k : ℕ) (hk : k < n),
    P (f ⟨k, hk⟩) → get_maximal_sat' P f (k+1) (nat.succ_le_of_lt hk) = some ⟨k, hk⟩ :=
begin
  intros k hkn hkP, dsimp [get_maximal_sat'],
  rw if_pos, refl, assumption
end

lemma get_maximal_sat'_spec_some2 {α} {n : ℕ} (P : α → Prop) [decidable_pred P] (f : fin n → α)
  : ∀ (k : ℕ) (hk : k ≤ n) (x : fin n),
    get_maximal_sat' P f k hk = some x
    → P (f x) :=
begin
  intros k hk x hx, induction k with k ih,
  { contradiction },
  { by_cases P (f ⟨k, hk⟩),
    { rw get_maximal_sat'_spec_some1 P f k hk h at hx,
      cases hx, assumption, },
    { simp [get_maximal_sat'] at hx, rw if_neg h at hx,
      apply ih, assumption } }
end

lemma get_maximal_sat'_spec_some3 {α} {n : ℕ} (P : α → Prop) [decidable_pred P] (f : fin n → α)
  : ∀ (k : ℕ) (hk : k ≤ n) (x : fin n),
    get_maximal_sat' P f k hk = some x
    → x.val < k :=
begin
  intros k hk x hx, induction k with k ih,
  { contradiction },
  { by_cases P (f ⟨k, hk⟩),
    { rw get_maximal_sat'_spec_some1 P f k hk h at hx,
      cases hx, simp, apply nat.lt_succ_self },
    { simp [get_maximal_sat'] at hx, rw if_neg h at hx,
      transitivity k, apply ih, assumption, apply nat.lt_succ_self } }
end

lemma get_maximal_sat'_spec_some4 {α} {n : ℕ} (P : α → Prop) [decidable_pred P] (f : fin n → α)
  : ∀ (k : ℕ) (hk : k ≤ n) (x : fin n) (y : fin n),
    get_maximal_sat' P f k hk = some x
    → y.val < k → P (f y) → y.val ≤ x.val :=
begin
  intros k, induction k with k ih; intros hk x y hx hylt hy,
  { contradiction },
  { by_cases P (f ⟨k, hk⟩),
    { rw get_maximal_sat'_spec_some1 P f k hk h at hx,
      cases hx, simp,
      apply nat.le_of_lt_succ,
      assumption },
    { dsimp [get_maximal_sat'] at hx,
      rw if_neg h at hx, apply ih, assumption',
      apply nat.lt_of_le_and_ne, apply nat.le_of_lt_succ hylt,
      intro h, subst h, apply h,
      rw (_ : fin.mk y.val hk = y),
      assumption, cases y, refl } }
end

/-
case 1: f x < n for all x
case 2: f x = n for exactly one x
case 2: f x = n for two values of x
-/

inductive pigeon_cases {α β} (P : β → Prop) (f : α → β)
| none_sat : (∀ x : α, ¬ P (f x)) → pigeon_cases
| one_sat : ∀ x, P (f x) → (∀ y, P (f y) → y = x) → pigeon_cases
| more_than_one_sat : ∀ x y, x ≠ y → P (f x) → P (f y) → pigeon_cases

def get_pigeon_cases (n : ℕ) (f : fin (n+2) → fin (n+1)) : pigeon_cases (λ x : fin (n+1), x.val = n) f :=
  if h : option.is_some (get_maximal_sat' (λ x : fin (n+1), x.val = n) f (n+2) (nat.le_refl _))
  then have h1 : get_maximal_sat' (λ x : fin (n+1), x.val = n) f (n+2) (nat.le_refl _) = some (option.get h),
       by apply option.eq_some_of_get,
       have h2 : (f (option.get h)).val = n,
       from get_maximal_sat'_spec_some2 (λ x : fin (n+1), x.val = n) f (n + 2) (le_refl _) (option.get h) h1,
       if h' : option.is_some (get_maximal_sat' (λ x : fin (n+1), x.val = n) f (option.get h).val (nat.le_of_lt (option.get h).is_lt))
       then have h3 : get_maximal_sat' (λ x : fin (n+1), x.val = n) f (option.get h).val (nat.le_of_lt (option.get h).is_lt) = some (option.get h'),
            by apply option.eq_some_of_get ,
            have h4 : (f (option.get h')).val = n,
            from get_maximal_sat'_spec_some2 (λ x : fin (n+1), x.val = n) f (option.get h).val (nat.le_of_lt (option.get h).is_lt) (option.get h') h3,
            pigeon_cases.more_than_one_sat (option.get h) (option.get h')
                                           (by { intro h'', apply nat.lt_irrefl (option.get h').val,
                                                 have := get_maximal_sat'_spec_some3 (λ x : fin (n+1), x.val = n) f (option.get h).val _ (option.get h') _, 
                                                 apply nat.lt_of_lt_of_le, assumption,
                                                 apply nat.le_of_eq, apply fin.veq_of_eq h'',
                                                 apply nat.le_of_lt, exact (option.get h).is_lt,
                                                 assumption })
                                            h2 h4
       else have h3 : get_maximal_sat' (λ x : fin (n+1), x.val = n) f (option.get h).val (nat.le_of_lt (option.get h).is_lt) = none,
            from option.eq_none_of_not_is_some h',
            have h4 : ∀ j (hj : j < (option.get h).val), ¬ ((f ⟨j, nat.lt_trans hj (option.get h).is_lt⟩).val = n),
            by { rw get_maximal_sat'_spec_none at h3, assumption },
            @pigeon_cases.one_sat _ _ (λ x : fin (n+1), x.val = n) f (option.get h) h2
              $ by { intros y hfy, cases y with y hy,
                     apply fin.eq_of_veq, apply nat.le_antisymm,
                     apply get_maximal_sat'_spec_some4 _ f _ _ _ _ h1; assumption,
                     apply le_of_not_gt, intro h,
                     rw get_maximal_sat'_spec_none at h3,
                     apply h3; assumption }
  else have h1 : get_maximal_sat' (λ x : fin (n+1), x.val = n) f (n+2) (nat.le_refl _) = none,
       from option.eq_none_of_not_is_some h,
       have h2 : ∀ j (hj : j < n+2), ¬ ((f ⟨j, hj⟩).val = n),
       by { rw get_maximal_sat'_spec_none at h1, assumption },
       pigeon_cases.none_sat (by { intro x, cases x, apply h2 })

structure collision {α β} (f : α → β) :=
(x y : α) (val_neq : x ≠ y) (f_eq : f x = f y)

def fin.coe_around {n} (x : fin (n+1)) (y : fin n) : fin (n+1) :=
  if y.val < x.val
  then y.up
  else y.succ

lemma fin.coe_around_neq {n} (x : fin (n+1)) (y : fin n)
  : fin.coe_around x y ≠ x :=
begin
  dsimp [fin.coe_around],
  by_cases y.val < x.val,
  { rw if_pos h, intro h', have h' := fin.veq_of_eq h',
    rw fin.up_val at h', rw h' at h, apply nat.lt_irrefl, assumption },
  { rw if_neg h, intro h', have h' := fin.veq_of_eq h',
    by_cases y.val > x.val,
    { rw ← h' at h,
      rw fin.succ_val at h, apply nat.lt_irrefl (y.val + 1),
      transitivity y.val, assumption, apply nat.lt_succ_self },
    { suffices : y.val = x.val, rw [fin.succ_val, this] at h',
      apply nat.succ_ne_self, assumption,
      cases (nat.eq_or_lt_of_not_lt _), assumption,
      contradiction, contradiction } }
end

lemma fin.coe_around_inj {n} (x : fin (n+1))
  : function.injective (fin.coe_around x) :=
begin
  intros a b hab, dsimp [fin.coe_around] at hab,
  by_cases ha : a.val < x.val; by_cases hb : b.val < x.val,
  { rw [if_pos, if_pos] at hab, 
    apply fin.eq_of_veq, have h' := fin.veq_of_eq hab,
    rw [fin.up_val, fin.up_val] at h', assumption' },
  { rw [if_pos, if_neg] at hab, exfalso,
    have h' := fin.veq_of_eq hab,
    rw [fin.up_val, fin.succ_val] at h',
    apply hb, transitivity b.val + 1,
    apply nat.lt_succ_self, rw ← h', assumption' },
  { rw [if_neg, if_pos] at hab, exfalso,
    have h' := fin.veq_of_eq hab,
    rw [fin.up_val, fin.succ_val] at h',
    apply ha, transitivity a.val + 1,
    apply nat.lt_succ_self, rw h', assumption' },
  { rw [if_neg, if_neg] at hab, 
    apply fin.eq_of_veq, have h' := fin.veq_of_eq hab,
    rw [fin.succ_val, fin.succ_val] at h',
    apply nat.succ_inj, assumption' }
end

def fin.restrict {n} (f : fin (n+2) → fin (n+1)) 
  (x : fin (n+2)) (h : ∀ y : fin (n+2), (f y).val = n → y = x)
  : fin (n + 1) → fin n :=
  λ y, fin.down (f (fin.coe_around x y)) (λ h', fin.coe_around_neq x y $ h _ h')

def fin.coll_of_restr_coll {n} (f : fin (n+2) → fin (n+1)) 
  (x : fin (n+2)) (h : ∀ y : fin (n+2), (f y).val = n → y = x)
  : collision (fin.restrict f x h) → collision f
| ⟨a, b, val_neq, f_eq⟩ := { collision . 
  x := fin.coe_around x a,
  y := fin.coe_around x b,
  val_neq := λ hxy, val_neq (fin.coe_around_inj x hxy),
  f_eq := by { dsimp [fin.restrict] at f_eq,
               apply fin.down_inj, assumption } }

def pigeonhole : ∀ (n : ℕ) (f : fin (n+1) → fin n), collision f
| 0 := λ f, fin.elim0 (f 0)
| (n+1) := λ f, match get_pigeon_cases n f with
                | pigeon_cases.none_sat hnone := 
                  fin.coll_of_restr_coll f ⟨n+1, nat.lt_succ_self _⟩ (λ y hy, false.elim $ hnone y hy)
                  $ pigeonhole n (fin.restrict f ⟨n+1, nat.lt_succ_self _⟩
                                    (λ y hy, false.elim $ hnone y hy))
                | pigeon_cases.one_sat x hx hno_other := 
                  fin.coll_of_restr_coll f x hno_other
                  $ pigeonhole n (fin.restrict f x hno_other)
                | pigeon_cases.more_than_one_sat x y hxy hx hy := 
                  ⟨x, y, hxy, fin.eq_of_veq $ eq.trans hx hy.symm⟩
                end

power.lean

definition nat_power {G} [group G] (g : G) : ℕ → G
| 0 := 1
| (n+1) := g * nat_power n

instance group_pow {G} [group G] : has_pow G ℕ := ⟨nat_power⟩

lemma nat_power.zero {G} [group G] (g : G)
  : g^0 = 1 := rfl

lemma nat_power.stepL {G} [group G] (g : G) (n : ℕ)
  : g^(n + 1) = g * g^n := rfl

lemma nat_power.one {G} [group G] (g : G)
  : g^1 = g := eq.trans (nat_power.stepL g 0) (mul_one g) 

lemma nat_power.stepR {G} [group G] (g : G)
  : ∀ (n : ℕ), g^(n + 1) = g^n * g 
| 0 := calc g^(0 + 1) = g^1 : congr_arg _ (zero_add _)
            ...       = g : nat_power.one g
            ...       = 1 * g : eq.symm (one_mul g)
            ...       = g^0 * g : congr_arg (λ x, x * g) (nat_power.zero g)
| (n+1) := calc g^(n + 2) = g * g^(n+1)   : nat_power.stepL g (n+1)
                ...       = g * (g^n * g) : congr_arg (λ x, g * x) $ nat_power.stepR n
                ...       = (g * g^n) * g : eq.symm $ mul_assoc _ _ _
                ...       = g^(n+1) * g   : @congr_arg _ _ (g * g^n) (g^(n+1)) (λ x, x * g) $ eq.symm $ nat_power.stepL g n

definition int_power {G} [group G] (g : G) : ℤ → G
| (int.of_nat n) := g ^ n
| -[1+ n] := (g ^ (n+1))⁻¹

infix `^^`:1024 := int_power

lemma int_power.zero {G} [group G] (g : G)
  : g^^0 = 1 := rfl

lemma int_power.neg {G} [group G] (g : G)
  : ∀ n : ℤ, g^^(-n) = (g^^n)⁻¹ := 
begin
  intro n, cases n,
  { cases n, transitivity g^^(int.of_nat 0), refl,
    transitivity g^0, refl, transitivity (g^0)⁻¹,
    rw nat_power.zero, rw one_inv, refl,
    rw int.neg_of_nat_of_succ,
    transitivity (nat_power g (n+1))⁻¹, refl, refl },
  { transitivity (g ^ (n+1))⁻¹⁻¹, 
    rw inv_inv, refl, refl }
end

lemma int_power.of_nonneg {G} [group G] (g : G)
  : ∀ n : ℤ, 0 ≤ n → g^^n = g^(int.nat_abs n) := 
begin
  intros n h, transitivity g^^(int.nat_abs n),
  congr, apply int.eq_nat_abs_of_zero_le h, refl
end

lemma int_power.of_neg {G} [group G] (g : G)
  : ∀ n : ℤ, n ≤ 0 → g^^n = (g^(int.nat_abs n))⁻¹ := 
begin
  intros, transitivity (g^^(int.nat_abs n))⁻¹,
  rw ← int_power.neg, congr,
  apply eq_neg_of_eq_neg, symmetry,
  rw ← int.nat_abs_neg n,
  apply int.eq_nat_abs_of_zero_le,
  apply neg_nonneg_of_nonpos, assumption,
  refl
end

lemma int_power.stepL {G} [group G] (g : G) (n : ℤ)
  : g^^(n + 1) = g * g^^n :=
begin
  cases le_or_gt 0 n,
  { transitivity g^(int.nat_abs (n + 1)),
    apply int_power.of_nonneg,
    transitivity (1 : ℤ), exact int.one_nonneg,
    apply le_add_of_nonneg_left, assumption,
    rw int.nat_abs_add_nonneg, rw int.nat_abs_one,
    rw nat_power.stepL, rw int_power.of_nonneg,
    assumption', exact int.one_nonneg },
  { cases n, cases h,
    rw int.neg_succ_of_nat_eq at h ⊢,
    rw int_power.of_neg g (-(↑n + 1)),
    rw int.nat_abs_neg,
    transitivity g * (g^(n + 1))⁻¹,
    rw [nat_power.stepR, mul_inv_rev, ← mul_assoc],
    rw [mul_inv_self, one_mul],
    transitivity (g^(int.nat_abs (-n)))⁻¹,
    rw ← int_power.of_neg,
    rw [neg_add, add_assoc, neg_add_self, add_zero],
    apply neg_le_of_neg_le, rw neg_zero,
    apply int.of_nat_nonneg,
    rw int.nat_abs_neg, rw int.nat_abs_of_nat,
    congr, apply le_of_lt, assumption }
end

lemma int_power.stepR {G} [group G] (g : G) (n : ℤ)
  : g^^(n + 1) = g^^n * g :=
begin
  cases le_or_gt 0 n,
  { transitivity g^(int.nat_abs (n + 1)),
    apply int_power.of_nonneg,
    transitivity (1 : ℤ), exact int.one_nonneg,
    apply le_add_of_nonneg_left, assumption,
    rw int.nat_abs_add_nonneg, rw int.nat_abs_one,
    rw nat_power.stepR, rw int_power.of_nonneg,
    assumption', exact int.one_nonneg },
  { cases n, cases h,
    rw int.neg_succ_of_nat_eq at h ⊢,
    rw int_power.of_neg g (-(↑n + 1)),
    rw int.nat_abs_neg,
    transitivity (g^(n + 1))⁻¹ * g,
    rw [nat_power.stepL, mul_inv_rev],
    rw [mul_assoc, mul_left_inv, mul_one],
    transitivity (g^(int.nat_abs (-n)))⁻¹,
    rw ← int_power.of_neg,
    rw [neg_add, add_assoc, neg_add_self, add_zero],
    apply neg_le_of_neg_le, rw neg_zero,
    apply int.of_nat_nonneg,
    rw int.nat_abs_neg, rw int.nat_abs_of_nat,
    congr, apply le_of_lt, assumption }
end

lemma int_power.one {G} [group G] (g : G)
  : g^1 = g := eq.trans (nat_power.stepL g 0) (mul_one g) 

lemma nat_power.add_eq_mul_pow {G} [group G] (g : G)
  : ∀ n m : ℕ, g^(n + m) = g^n * g^m
| 0 m := eq.trans (eq.symm (one_mul (g^(0 + m)))) (congr_arg _ (congr_arg _ (zero_add m)))
| (n+1) m := calc g^(n + 1 + m) = g^(n + m + 1)   : congr_arg _ (nat.add_right_comm _ _ _)
                  ...           = g * (g^n * g^m) : congr_arg (λ x, g * x) (nat_power.add_eq_mul_pow n m)
                  ...           = (g * g^n) * g^m : eq.symm $ mul_assoc _ _ _

lemma pow_nonneg_int_eq_pow {G} [group G] (g : G) (n : ℤ) 
  : n ≥ 0 → g^^n = g^(int.nat_abs n) :=
begin
  intro h, transitivity g^^(int.of_nat (int.nat_abs n)),
  congr, apply int.eq_nat_abs_of_zero_le h, refl
end

lemma pow_neg_int_eq_inv_pow {G} [group G] (g : G) (n : ℤ) 
  : n < 0 → g^^n = (g^(int.nat_abs n))⁻¹ :=
begin
  intro h, cases int.eq_neg_succ_of_lt_zero h,
  rw h_1, refl
end

lemma int_power.add_nat_eq_mul_pow {G} [group G] (g : G)
    : ∀ (n : ℤ) (k : ℕ), g^^(n + k) = g^^n * g^k :=
begin
  intros, induction k with k ih,
  { transitivity g^^(n + 0), refl,
    rw [add_zero, nat_power.zero, mul_one] },
  { transitivity g^^(n + int.of_nat (k + 1)), refl,
    rw int.of_nat_add k 1, rw ← add_assoc,
    rw (_ : int.of_nat 1 = 1), rw int_power.stepR, 
    transitivity g^^(n + k) * g, refl,
    rw ih, rw mul_assoc, rw nat_power.stepR, refl }
end

lemma int_power.nat_add_eq_mul_pow {G} [group G] (g : G)
    : ∀ (k : ℕ) (n : ℤ), g^^(k + n) = g^k * g^^n :=
begin
  intros, induction k with k ih,
  { transitivity g^^(0 + n), refl,
    rw [zero_add, nat_power.zero, one_mul] },
  { transitivity g^^(int.of_nat (k + 1) + n), refl,
    rw int.of_nat_add k 1, rw add_right_comm,
    rw (_ : int.of_nat 1 = 1), rw int_power.stepL,
    transitivity g * g^^(k + n), refl,
    rw ih, rw ← mul_assoc, rw nat_power.stepL, refl }
end

lemma int_power.add_eq_mul_pow {G} [group G] (g : G) 
  : ∀ n m : ℤ, g^^(n + m) = g^^n * g^^m :=
begin
  intros,
  by_cases h1 : n ≥ 0; by_cases h2 : m ≥ 0,
  { repeat { rw pow_nonneg_int_eq_pow },
    rw int.nat_abs_add_nonneg, 
    apply nat_power.add_eq_mul_pow,
    assumption', apply add_nonneg h1 h2 },
  { rw int.eq_nat_abs_of_zero_le h1,
    apply int_power.nat_add_eq_mul_pow },
  { rw int.eq_nat_abs_of_zero_le h2,
    apply int_power.add_nat_eq_mul_pow },
  { have h1 := lt_of_not_ge h1, have h2 := lt_of_not_ge h2,
    repeat { rw pow_neg_int_eq_inv_pow },
    rw int.nat_abs_add_neg,
    rw [← mul_inv_rev, ← nat_power.add_eq_mul_pow],
    rw nat.add_comm, assumption', apply add_neg h1 h2, }
end

lemma int_power.sub_mul {G} [group G] (g : G)
  : ∀ n m : ℤ, g^^(n - m) * g^^m = g^^n :=
by { intros, rw sub_eq_add_neg,
     rw int_power.add_eq_mul_pow,
     rw mul_assoc, rw int_power.neg,
     rw [mul_left_inv, mul_one] }

def order_bound_of_pow_not_inj {G} [group G] (g : G)
  : ∀ n m : ℤ, g^^n = g^^m → g^^(n - m) = 1 := λ n m h,
calc g^^(n - m) = g^^(n - m) * 1 : eq.symm (mul_one _)
     ...        = g^^(n - m) * (g^^m * (g^^m)⁻¹) : by { rw mul_inv_self }
     ...        = (g^^(n - m) * g^^m) * (g^^m)⁻¹ : eq.symm $ mul_assoc _ _ _
     ...        = g^^n * (g^^m)⁻¹ : by rw int_power.sub_mul
     ...        = g^^n * (g^^n)⁻¹ : by rw h
     ...        = 1 : mul_inv_self _