/- Clara L"oh 2021 -/

import tactic -- standard proof tactics
import algebra.group.basic -- basic group theory
open finset   -- for range operator
open_locale big_operators -- to enable ∑ notation


open classical -- we want to work in classical logic


/- Exercise 1 -/

-- the sum of the natural numbers 0,...,n
def first_nat_sum
  : nat → nat
| 0            := -- add definition
| (nat.succ n) := -- add definition

-- ... and its value in closed form
lemma first_nat_sum_eval
      (n : nat)
    : first_nat_sum n = n * (n+1)
:=
begin
  -- we prove this claim by induction (over the natural number arugment n)
  induction n with m ind_hyp,

  -- base case: 0
  case nat.zero : {sorry},

  -- induction step: m -> m+1 with induction hypothesis ind_hyp
  case nat.succ : 
  begin

    sorry,

  end
end     

-- alternatively: using ∑ (optional)

/-

def first_nat_sum'
  : nat → nat
:= λ n, 2 * ∑ (i : nat) in range (n+1), -- complete definition

lemma first_nat_sum'_eval
      (n : nat)
    : first_nat_sum' n = n * (n+1)
:=
begin
  have rw_sum : first_nat_sum' = λ n : nat, ∑ (i : nat) in range (n+1), 2 * i, from
  begin

    sorry,

    -- unfold, ext1, and library_search might help    
  end,

  -- induction proof, using rw_sum
  -- sum_range_succ might help
  induction n with m ind_hyp,

end      

-/

/- Exercise 2 -/

lemma powers_of_conjugates
      (G : Type*) [group G]
      (a : G)
      (b : G)
      (n : nat)
    : -- complete statement
:=
begin
  -- we prove this claim by induction (over the natural number arugment n)

  sorry,

end      

lemma commuting_powers 
      (G : Type*) [group G]
      (a : G)
      (b : G)
      -- complete the hypotheses
      (n : nat)
    : -- complete the statemnt
:=
begin

   sorry,

end