How is `IsCancelAdd (Fin n)` implemented?

Stream: mathlib4

[Hanting Zhang]

The core theorem seems to be defined here:

/-- Note this is more general than `Fin.addCommGroup` as it applies (vacuously) to `Fin 0` too. -/
instance instIsCancelAdd (n : ℕ) : IsCancelAdd (Fin n) where
  add_left_cancel := Nat.casesOn n finZeroElim fun _i _ _ _ ↦ add_left_cancel
  add_right_cancel := Nat.casesOn n finZeroElim fun _i _ _ _ ↦ add_right_cancel

But I'm failing to understand how the proof is even correct. How does the final add_{left|right}_cancel at the end complete the proof?

I tried my own implementation of MyFin to try and step through each part, like this:

structure MyFin (n : Nat) where
  mk ::
  val  : Nat
  isLt : LT.lt val n

theorem myMlt {n b : Nat} : {a : Nat} → a < n → b % n < n
  | 0,   h => Nat.mod_lt _ h
  | _+1, h =>
    have : n > 0 := Nat.lt_trans (Nat.zero_lt_succ _) h;
    Nat.mod_lt _ this

def elim0.{v} {α : Sort v} : MyFin 0 → α
  | ⟨_, h⟩ => absurd h (Nat.not_lt_zero _)

/-- Addition modulo `n` -/
def myFinAdd {n : Nat} : MyFin n → MyFin n → MyFin n
  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + b) % n, myMlt h⟩

instance {n : Nat} : Add (MyFin n) where
  add := myFinAdd

/-- Elimination principle for the empty set `Fin 0`, dependent version. -/
def myFinZeroElim {α : MyFin 0 → Sort*} (x : MyFin 0) : α x :=
  elim0 x

-- set_option diagnostics true
/-- Note this is more general than `Fin.addCommGroup` as it applies (vacuously) to `Fin 0` too. -/
instance instIsCancelAdd (n : Nat) : IsCancelAdd (MyFin n) where
  add_left_cancel := Nat.casesOn n finZeroElim fun _i _ _ _ ↦ add_left_cancel
  add_right_cancel := Nat.casesOn n finZeroElim fun _i _ _ _ ↦ add_right_cancel

but then I get:

failed to synthesize
  IsLeftCancelAdd (MyFin _i.succ)
Additional diagnostic information may be available using the `set_option diagnostics true` command.Lean 4

So clearly there's something happening in the native Fin implementation that I'm missing and/or don't understand.

I have two main questions:

1. What is missing from my dummy example that would make it work?
2. How does the native implementation work? (Possibly very related to (1).)

Thank you!

[Eric Wieser]

1. You implement AddCommGroup (Fin n.succ) first
2. It implements AddCommGroup (Fin n.succ) first