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

def plus ( m n : Nat ) := match m with
| .zero => n
| .succ m => Nat.succ ( plus m n )

/- Lean understands the usual abbreviations for
Nat.succ ( Nat.succ ( ... ( Nat.succ ( Nat.zero ) ) ... ) ) -/

#eval plus 0 0
#eval plus 1 3
#eval plus 2 11

/- You can write n.succ instead of Nat.succ n -/

#eval Nat.zero.succ

theorem zero_plus ( n : Nat ) : plus 0 n = n := by
  sorry

theorem plus_zero ( m : Nat ) : plus m 0 = m := by
  sorry

theorem plus_succ ( m n : Nat ) : plus m n.succ = (plus m n).succ := by
  sorry