macro "conj_elim" hp:ident hq:ident "from" h:ident : tactic =>
  `(tactic|(have ⟨$hp,$hq⟩ := $h))

macro "conj_intro" h:ident "from" hp:ident hq:ident : tactic =>
  `(tactic|(have $h : _∧_ := And.intro $hp $hq))

macro "disj_elim" hp:ident hq:ident "from" h:term:arg : tactic =>
  `(tactic|(refine Or.elim $h (fun $hp => ?_) (fun $hq => ?_)))

macro "disj_intro_left" h:ident "from" hp:ident q:term:arg : tactic =>
  `(tactic|(have $h : _∨($q) := Or.inl $hp))

macro "disj_intro_right" h:ident "from" p:term:arg hq:ident : tactic =>
  `(tactic|(have $h : ($p)∨_ := Or.inr $hq))

macro "impl_elim" hq:ident "from" hp:ident hpq:ident : tactic =>
  `(tactic|(have $hq := $hpq $hp))

namespace And
theorem elim' {P Q : Prop} {R : Sort} (h : P ∧ Q) (f : P → Q → R) : R := by
  sorry
end And

namespace Nat

def plus : Nat → Nat → Nat := by
  intro m n
  induction m
  case zero =>
    exact n
  case succ m p =>
    exact succ p


#eval plus 0 0
#eval plus 2 2
#eval plus 3 5

example : plus 2 2 = 4 := by
  sorry


def times_two : Nat → Nat := by
  intro m
  induction m
  case zero =>
    exact zero
  case succ m p =>
    exact p.succ.succ


#eval times_two 0
example : times_two 0 = 0 := by
  sorry

#eval times_two 1
example : 
    times_two 1 = 2 := by
  sorry

#eval times_two 2
example :
    times_two 2 = 4 := by
  sorry

def times : Nat → Nat → Nat := by
  intro m n
  induction m
  case zero =>
    exact zero
  case succ m p =>
    exact ( plus n p )

#eval times 2 2
example : times 2 2 = 4 := by
  sorry


#eval times 3 5
example : times 3 5 = 15 := by
  sorry