gistfile1.txt

definition blocking_add (N₁ N₂ : ℕ) : ℕ := N₁ + N₂

theorem foo {N : ℕ} {a b : fin N}
    : a^.val + b^.val = b^.val + a^.val
:= nat.add_comm _ _

theorem bar {N : ℕ} (a : fin (nat.succ N)) (b : fin (N + 1))
    : a^.val + b^.val = b^.val + a^.val
:= by rw foo

theorem baz {N : ℕ} (a : fin (nat.succ N)) (b : fin (blocking_add N 1))
    : a^.val + b^.val = b^.val + a^.val
:= begin
     --rw foo                       -- does not work
     --rw @foo (nat.succ N) a b     -- does not work
     --unfold blocking_add, rw foo  -- works
     --apply foo                    -- works
   end