@markusde @maxsnew
A+++ great work

but wait ok I am worried I'm not seeing all the foot-rakes present here. I know about Fin literal wrapping, and saturating subtraction, but

((3 : Nat) * n) / n

is fine... isn't it?

theorem markusde_cant_fool_me (x n : ℕ) (h : n ≠ 0): (x * n) / n = x :=
Eq.symm (Nat.eq_div_of_mul_eq_left h rfl)

or are you just deliberately sowing some reasonable examples among the surprising to keep us all on our toes

@jcreed @maxsnew
> (n : ℕ) (h : n ≠ 0)

Good! I didn't tell you the type of N, but you inferred that it should probably be a natural number, and you probably need a side condition about it being nonzero.

You correctly did _not_ infer that N was some nonzero-by-construction type which would avoid that side condition at the expense of becoming completely bizarre.